[SystemSafety] CbyC and unit testing

[Olwen Morgan]

Thank you again for helpful observations. My reactions are interspersed:

On 06/07/2020 18:37, Martyn Thomas wrote:
> On 05/07/2020 12:47, Olwen Morgan wrote:
>> Does anyone here honestly believe that you could successfully defend
>> omitting UT in an action for negligence if a system developed using
>> CbyC failed and killed someone as a result of a defect that could have
>> been detected by UT?
> Can you guarantee that your UT will detect all the errors that any
> possible UT would have detected? If so, how?
No, you cannot guarantee that UT will detect any error. What I am saying 
is that there are circumstances in which it gives you the first 
opportunity to detect errors that the upstream tools might have missed.
> Are you using successful tests as the axioms on which you can develop a
> rigorous inductive proof of correctness, which (if I recall correctly)
> Tony Hoare said was how testing should be used?
I regard the notion of "rigorous inductive proof" as meaningless in this 
context. I have difficulty with the application of the term "rigorous" 
to testing since it invites, IMO, a false comparison with the rigour 
with which CbyC proofs are carried out. My own personal practice is, as 
I have said, to code my units such that any set of tests that achieves 
100% strong, robust, boundary value coverage (taking both 
formally-referenced-black-box and white-box-internal data into account) 
also achieves 100% simple path coverage. This is to assure a very 
high-level of relevant coverage in testing and typically involves a 
pseudo-single-assignment style in which every variable is declared in 
the smallest possible scope, is initialised at declaration and is 
threatened by assignment in at most one point in its scope. It tends to 
resemble functional programming in structure and is indeed intended to 
do so on the assumption (possibly unwarranted) that it tends to make 
life easier for any prover. This is a major consideration in C where, if 
you are striving for best attainable practice, you might be using 
several different verification tools. AFAI can see, this is a far 
stronger requirement than I've ever heard anyone else use or advocate. 
If this was what CARH was getting at in the notion of "rigorous 
inductive proof", then that's what I'm doing. I reached this practice as 
a result of developing a somewhat technically paranoid mindset when 
working in C system development.
>
> If not, in your hypothetical example, how are you going to defend having
> omitted the unit tests that would have detected the errors that caused
> the failure that killed someone?

I wouldn't defend it. It is IMO utterly indefensible. UT may have its 
weaknesses but it is IMO negligent to omit it if it would provide the 
first opportunity to detect errors missed upstream. It is not guaranteed 
to detect such errors but if you do it (ultra-)systematically, it may 
stand a very good chance of doing so.


> I think you are doing what the opponents of FMs often do and assuming
> that the proponent of C-by-C is claiming they can deliver perfection.
> I'm certainly not - I'm saying that software engineering seeks to make
> software that is as fit as is reasonably practicable for it's intended
> purpose and that in my experience, being as rigorous as reasonably
> practicable is tautologically how to achieve that.
I'm not doing that. I do not oppose formal methods. I support and 
advocate them. What I oppose is the making of unguarded, unqualified 
statements such as PBL's that are wide open to misinterpretation by the 
great unwashed.
> In my experience, most software teams don't even try to be rigorous. At
> best they are skilled craftspeople, not professional engineers.
> Sometimes that's good enough. Sometimes it may even be what you need.
> Caveat emptor.
My experience is the same and I've worked with unqualified software 
developers who have IMO performed better than qualified and chartered 
professionals, so I'd never banish the craftspeople by fiat.


Hopefully we might now generating more light than heat?


Olwen