<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40"><head><meta http-equiv=Content-Type content="text/html; charset=utf-8"><meta name=Generator content="Microsoft Word 15 (filtered medium)"><style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
{font-family:Consolas;
panose-1:2 11 6 9 2 2 4 3 2 4;}
@font-face
{font-family:FreeSans;
panose-1:0 0 0 0 0 0 0 0 0 0;}
@font-face
{font-family:"DejaVu Sans";
panose-1:0 0 0 0 0 0 0 0 0 0;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
pre
{mso-style-priority:99;
mso-style-link:"HTML Preformatted Char";
margin:0cm;
margin-bottom:.0001pt;
font-size:10.0pt;
font-family:"Courier New";}
span.HTMLPreformattedChar
{mso-style-name:"HTML Preformatted Char";
mso-style-priority:99;
mso-style-link:"HTML Preformatted";
font-family:Consolas;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]--></head><body lang=EN-CA link="#0563C1" vlink="#954F72"><div class=WordSection1><p class=MsoNormal><span style='mso-fareast-language:EN-US'>In fairness a client report would usually include caveats about the use of the statements contained therein and would usually be part of a contract which from personal experience will also define how comments from a client can, and should, be used. Taking an email comment out of context and extrapolating it to be equivalent to a conclusion contained in a client report is a little unrealistic.<o:p></o:p></span></p><p class=MsoNormal><span style='mso-fareast-language:EN-US'><o:p> </o:p></span></p><p class=MsoNormal><span style='mso-fareast-language:EN-US'>Andy<o:p></o:p></span></p><p class=MsoNormal><span style='mso-fareast-language:EN-US'><o:p> </o:p></span></p><div><div style='border:none;border-top:solid #E1E1E1 1.0pt;padding:3.0pt 0cm 0cm 0cm'><p class=MsoNormal><b><span lang=EN-US>From:</span></b><span lang=EN-US> systemsafety <systemsafety-bounces@lists.techfak.uni-bielefeld.de> <b>On Behalf Of </b>Olwen Morgan<br><b>Sent:</b> July 4, 2020 4:52 PM<br><b>To:</b> systemsafety@lists.techfak.uni-bielefeld.de<br><b>Subject:</b> [SystemSafety] CbyC and unit testing<o:p></o:p></span></p></div></div><p class=MsoNormal><o:p> </o:p></p><p><o:p> </o:p></p><p><span style='font-family:"FreeSans",serif'>FWIW here is what PBL said and what I think, in a more guarded moment, he should have said:</span><o:p></o:p></p><p><o:p> </o:p></p><p><span style='font-family:"FreeSans",serif'>1. What PBL said:</span><o:p></o:p></p><pre><span style='font-family:"FreeSans",serif'>"If the programmer [is] using CbyC methods/tools such as in SPARK Pro appropriately, then the<o:p></o:p></span></pre><pre><span style='font-family:"FreeSans",serif'>program does indeed do what the specification says (modulo discharging proof obligations), which is<o:p></o:p></span></pre><pre><span style='font-family:"FreeSans",serif'>the point of unit testing the various components. Thereby unit testing can be avoided if you use CbyC."<o:p></o:p></span></pre><pre><span style='font-family:"FreeSans",serif'><o:p> </o:p></span></pre><pre><span style='font-family:"FreeSans",serif'><o:p> </o:p></span></pre><pre><span style='font-family:"FreeSans",serif'>2. What I think he might better have said to mitigate the risks of serious misinterpretation:<o:p></o:p></span></pre><pre><span style='font-family:"FreeSans",serif'><o:p> </o:p></span></pre><pre><span style='font-family:"FreeSans",serif'>"If the programmer [is] using CbyC methods/tools such as in SPARK Pro appropriately, then, subject to qualifications that include the following:<o:p></o:p></span></pre><pre><span style='font-family:"FreeSans",serif'>...<o:p></o:p></span></pre><pre><span style='font-family:"FreeSans",serif'><list of qualifications><o:p></o:p></span></pre><pre><span style='font-family:"FreeSans",serif'>...<o:p></o:p></span></pre><pre><span style='font-family:"FreeSans",serif'>it is highly probable that the program does indeed do what the specification says (modulo discharging proof obligations), which is<o:p></o:p></span></pre><pre><span style='font-family:"FreeSans",serif'>the point of unit testing the various components. Thereby the risk involved in omitting unit testing can be very small if you use CbyC."<o:p></o:p></span></pre><pre><o:p> </o:p></pre><pre><span style='font-family:"FreeSans",serif'>I'll address what the list of qualifications should contain in a later posting.<o:p></o:p></span></pre><pre><span style='font-family:"FreeSans",serif'><o:p> </o:p></span></pre><pre><span style='font-family:"FreeSans",serif'><o:p> </o:p></span></pre><pre><span style='font-family:"FreeSans",serif'>Honestly, If I'd put PBL's statement in a report to a client about the capabilities of CbyC, then I'd consider I had no defence at all against a charge of professional negligence if the client misinterpreted it, omitted UT when it was risky to do so, and his system, with undetected defects, consequently failed and killed someone.<o:p></o:p></span></pre><pre><span style='font-family:"FreeSans",serif'><o:p> </o:p></span></pre><pre><span style='font-family:"FreeSans",serif'><o:p> </o:p></span></pre><pre><span style='font-family:"FreeSans",serif'><o:p> </o:p></span></pre><pre><span style='font-family:"FreeSans",serif'>Jesus wept!<o:p></o:p></span></pre><pre><span style='font-family:"FreeSans",serif'><o:p> </o:p></span></pre><pre><span style='font-family:"FreeSans",serif'>Olwen<o:p></o:p></span></pre><pre><span style='font-family:"DejaVu Sans",serif'><o:p> </o:p></span></pre><pre><o:p> </o:p></pre></div></body></html>