[SystemSafety] CbyC and unit testing

[andy at the-ashworths.org]

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.

 

Andy

 

From: systemsafety <systemsafety-bounces at lists.techfak.uni-bielefeld.de> On Behalf Of Olwen Morgan
Sent: July 4, 2020 4:52 PM
To: systemsafety at lists.techfak.uni-bielefeld.de
Subject: [SystemSafety] CbyC and unit testing

 

 

FWIW here is what PBL said and what I think, in a more guarded moment,  he should have said:

 

1. What PBL said:

"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."
 
I'll address what the list of qualifications should contain in a later posting.
 
 
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!
 
Olwen
 
 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/pipermail/systemsafety/attachments/20200704/7ba7259b/attachment-0001.html>