Re: {Pre,Post}conditions and side effects

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Thu, 7 May 2015 14:01:34 -0500, 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?

You don't need to know it, to have it existing. (If a tree falls in a
forest and no one is around to hear it, does it make a sound?)

A correct program exists in the sense that there exist a combination of
characters that represents this program. Whether anybody is capable to
write this combination down is no matter. Moreover, the program exists in
strictly constructive terms. You can enumerate all possible programs and
some them will be correct. Even correctness proof is constructive because
the number of states of any program is finite. So you can always find a
correct program given enough time.

> If you 
> use some prover program, it too may have bugs.

Yes, but every programmer deals with partially correct program, he knows
which parts of the program are correct, which parts are known to be
incorrect and which parts are neither.

> Or there might be bad data (cosmic rays?)

Bad data do not make program incorrect. (If "bad" means "inputs I forgot to
think about" that is lousy problem analysis)

> Or the specification might be incomplete.

Oh, but that does not make its implementation incorrect. Incompleteness of
specification is not the program's property. (Be careful what you wish for,
it might come true)

> 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.

It is an infinite recursion, which is why it is meaningless to define
correctness, as you seem do, as some absolute. There cannot be such thing.
The program is correct when it agrees with the specified behavior. Period.
Whether the specification is itself correct, or if behavior is desired,
legal, moral, safe, haram etc is outside the scope.

> Ergo, I don't believe that "proper preconditions" really exist.

In the sense you try to put into it, yes, they do not exist. They do not
because you could not formalize it. There is no formal framework where you
could consistently formulate that idea. It is inherently inconsistent.

> And in the 
> rare cases that they do (perhaps because of an immediately preceding 
> postcondition), a compiler would have eliminated them anyway, so you're not 
> paying anything for the supposed runtime check. (After all, Ada compilers 
> have been aggressively removing checks since 1983; that's nothing new to an 
> Ada compiler writer.)

The point is that these are fundamentally different things. Correctness is
outside. Behavior is inside. You cannot convert one into another keeping
the program. Checks elimination is strictly about behavior, merely a
program transformation, optimization. Correctness evaluation is not
behavior, it is not the program at all.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de