[SystemSafety] CbyC and unit testing

[Olwen Morgan]

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/a0748c3c/attachment.html>