Re: {Pre,Post}conditions and side effects

[Stefan.Lucks@uni-weimar.de]

[-- Attachment #1: Type: TEXT/PLAIN, Size: 1710 bytes --]

On Thu, 7 May 2015, Randy Brukardt wrote:

> If the compiler fails to optimize the check away, your program is wrong in
> some sense, and you should have gotten an error or warning (depending on the
> compiler mode and exception contracts) to that effect.

I am a big fan of correctness proofs, where they are applicable. But 
logically,

   Not(Proven_Correct) /= Proven(Incorrect)

Furthermore, automatic theorem proving can only go so far. I may actually 
know my program to be correct -- and maybe I can even prove it manually. 
Why should the compiler reject my program, or insert useless checks, just 
because it fails to find the proof?

Warning or not I would consider a compiler (or a language) which generates 
linear-time code for binary search badly broken. Rejecting the program 
would be the lesser evil. Which would turn Ada into a new SPARK.

But then, the Ada standard would have to define the underlying theorem 
prover, for compatibility reasons. Else, the same program may be proven 
correct by one prover, where another prover fails.

> You ought to fix your
> program (probably by adding an appropriate predicate) so that the check
> *can* be eliminated (or pushed to somewhere where the cost is irrelevant).

Why do I need to fix the program, if I know it is correct? Just because 
the compiler isn't good enough at theorem proving?

>> Turning off the checks just hides the problem.

*IF* there is a problem at all.

Stefan


------  I  love  the  taste  of  Cryptanalysis  in  the morning!  ------
uni-weimar.de/de/medien/professuren/mediensicherheit/people/stefan-lucks
--Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany--