[SystemSafety] CbyC and unit testing
Olwen Morgan
olwen at phaedsys.com
Sat Jul 4 22:51:42 CEST 2020
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>
More information about the systemsafety
mailing list