[SystemSafety] Fetzer

[David Crocker]

Derek,

It appears to me that either you don't understand program verification,
or you are deliberately ignoring an important point, which is that an
unverified program is likely to contain a much larger number of errors
than the formal specification it implements, for several reasons:

1. Specification languages are designed with *safety in mind*, unlike
most programming languages. So the error rate for the specification per
1000 lines is likely to be lower than for the program.

2. A specification is (or should be) *much shorter* and less complex
than the program that implements it. So again, the specification should
contain many fewer errors.

3. Specifications can themselves be verified formally to some extent by
including redundancy. In Escher C/C++ Verifier, we do this by means of
generalised use cases. This is a function that states "given this
initial state and this sequence of inputs, I expect the system to
produce these outputs and be in this final state" where the outputs and
final state are functions of the input variable and initial state. So
once again, the specification should contain fewer errors, because it
has been checked against the user's expectations insofar as they have
been expressed.

So your "N-version with N=2" argument falls. What formal verification of
code against specifications does is to replace a large program that is
likely to contain many errors by a smaller specification which has
itself been verified to a greater or lesser extent and it likely to
contain many fewer errors.

I might add that constructing a formal specification it itself very
helpful in exposing ambiguity and uncertainty in the user's requirements.

David Crocker, Escher Technologies Ltd.
http://www.eschertech.com
Tel. +44 (0)20 8144 3265 or +44 (0)7977 211486

On 19/06/2019 15:19, Derek M Jones wrote:
> David,
>
>> nobody constructs program proofs by hand these days, except perhaps in
>> academia. Formal proofs of programs are always constructed either
>> completely automatically, or in a few cases using an interactive theorem
>> prover.
>
> This approach is essential N-version programming, with N=2.
>
> Two programs get written, one is nominated to be the specification,
> and a tool checks that the behavior of the two programs are consistent
> with each other.
>
> The correctness argument relies on a verbal slight of hand.  The
> program nominated to be the specification is deemed to be correct,
> because it's the specification.  If the second program has consistent
> behavior, compared to the 'specification', then it's said to be correct.
>
>> So the important question is: what is the error rate of
>> machine-constructed program proofs, produced by whatever tool is used to
>> generate them. I think this is akin to asking what is the rate of code
>
> There is a lot more to consider than the error rate of the tool.
>
> Particular tools are based on particular mathematical formalisms.  Which
> means they are not capable of detecting inconsistencies of a kind not
> supported by the formalism used, i.e., they look for a specific kind
> of inconsistency.
>
> As with all N-version solutions, the same incorrect behavior can occur
> in both programs being compared.
>
>> David Crocker, Escher Technologies Ltd.
>> http://www.eschertech.com
>> Tel. +44 (0)20 8144 3265 or +44 (0)7977 211486
>>
>> On 19/06/2019 13:54, Derek M Jones wrote:
>>> David,
>>>
>>> The idea that software can be proved correct is based on the
>>> assumption that mathematics is always correct.
>>>
>>> Plenty of mistakes get made in so called mathematical proofs.
>>> In some cases theorems are given with only an outline of a proof.
>>>
>>> And of course, a lot more people are running code, than checking
>>> mathematical proofs.  So more mistakes get found in code than
>>> mathematics.
>>>
>>> The continuing belief that mathematics can be used for proving
>>> software correct should be a fertile topic for social scientists
>>> and anthropologists, no need to visit 'primitive' tribes to
>>> find strange ideas, they are here under their noses.
>>>
>>> https://shape-of-code.coding-guidelines.com/2013/11/17/what-is-the-error-rate-for-published-mathematical-proofs/
>>>
>>>
>>>
>>> https://shape-of-code.coding-guidelines.com/2018/02/19/mathematical-proofs-contain-faults-just-like-software/
>>>
>>>
>>>
>> _______________________________________________
>> The System Safety Mailing List
>> systemsafety at TechFak.Uni-Bielefeld.DE
>> Manage your subscription:
>> https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20190619/9b0b2fcd/attachment.html>