[SystemSafety] Fetzer

[Derek M Jones]

Martyn,

> You overlook that important properties can be proved, such as the absence of overflow failures for any input combinations. No feasible amount of testing can give that assurance.

Yes, it is sometimes possible to show properties such as
bounds on the value of a variable.

The big practical issue is the substantial number of dependencies
between variables.  This often makes it very difficult to get
any useful results.  Does anybody have any data on the percentage
of variables whose possible bounds can be shown to be very restricted?

Perhaps the most interesting tool in this area is Daikon, which does
invariant detection based on values seen during program execution:
https://plse.cs.washington.edu/daikon/

Developers can then check the invariants, looking for unexpected
relationships.

> Regards
> 
> Martyn
> 
>> On 19 Jun 2019, at 15:19, Derek M Jones <derek at knosof.co.uk> 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
>>
>> -- 
>> Derek M. Jones           Software analysis
>> tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com
>> _______________________________________________
>> The System Safety Mailing List
>> systemsafety at TechFak.Uni-Bielefeld.DE
>> Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
> 
> 

-- 
Derek M. Jones           Software analysis
tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com