Re: {Pre,Post}conditions and side effects

[Niklas Holsti <niklas.holsti@tidorum.invalid>]

On 15-05-07 22:01 , Randy Brukardt wrote:
> <Stefan.Lucks@uni-weimar.de> wrote in message
> news:alpine.DEB.2.11.1505071909280.16448@debian...
> ...
>> One property of a proper precondition (or postcondition or ...) is that
>> disabling the check does not change the functional behaviour of correct
>> programs.
>
> Sure, but this is irrelevant. There are no "correct" programs (in all
> possible senses). How do you know that you have a correct program? If you
> use some prover program, it too may have bugs. Or there might be bad data
> (cosmic rays?)

Those are practical problems, not problems of principle. If you would 
take the same attitude to mathematics, you would claim that there are no 
correct theorems. So I disagree with you.

> Or the specification might be incomplete. Consider the latest
> Dreamliner issue; that probably wouldn't have been caught by a prover simply
> because no one would have included an appropriate assertion.

If it was an overflow problem (and not wrap-around of a modular type) 
CodePeer would probably have complained that it could not prove absence 
of overflow. That is, many failures result from violations of general 
assertions that one does not have to write explicitly.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .