<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body>
<p><br>
</p>
<p><font face="FreeSans">FWIW here is what PBL said and what I
think, in a more guarded moment, he should have said:</font></p>
<p><font face="FreeSans"><br>
</font></p>
<p><font face="FreeSans">1. What PBL said:<br>
</font></p>
<p> </p>
<pre class="moz-quote-pre" wrap=""><font face="FreeSans">"If the programmer [is] using CbyC methods/tools such as in SPARK Pro appropriately, then the
program does indeed do what the specification says (modulo discharging proof obligations), which is
the point of unit testing the various components. Thereby unit testing can be avoided if you use CbyC."
2. What I think he might better have said to mitigate the risks of serious misinterpretation:
"If the programmer [is] using CbyC methods/tools such as in SPARK Pro appropriately, then, subject to qualifications that include the following:
...
<list of qualifications>
...
it is highly probable that the program does indeed do what the specification says (modulo discharging proof obligations), which is
the point of unit testing the various components. Thereby the risk involved in omitting unit testing can be very small if you use CbyC."
</font>
<font face="FreeSans"><font face="FreeSans">I'll address what the list of qualifications should contain in a later posting.
</font>
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.
Jesus wept!
</font><font face="DejaVu Sans"><font face="FreeSans">
Olwen
</font>
</font>
</pre>
</body>
</html>