Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus <rm.dash-bauhaus@futureapps.de>]

On 05.07.12 10:48, Dmitry A. Kazakov wrote:
> On Wed, 4 Jul 2012 21:18:24 -0500, Randy Brukardt wrote:
> 
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
>> news:13hfxjlq0xqtq.x3v8evyf4pku$.dlg@40tude.net...
>>> On Mon, 2 Jul 2012 23:51:19 -0500, Randy Brukardt wrote:
>> ...
>>>> Legality has nothing to do with preconditions or postconditions.
>>>
>>> => It is OK to violate a "contract" defined by these. Here you are.
>>
>> No, it's not OK; that is the crux of our disagreement. You seem to think 
>> that the only kind of "contract" is some sort of static thing.
> 
> Exactly. Because the contract exists *before* any programs implementing it
> and after them. The contract exists even when there is no such program.

OK

> Therefore it cannot depend on the program state.

The "therefore" does not follow, because "it" makes too far reaching
assumptions, from which, I think, no one suggests your logic does not
follow. "It", for a start, once it materializes in this or that form.

Contract checking built into a program is rather
a design tool than some oracular inference engine.
Correctness need not be assumed at this stage.

If the checks are severely flawed bacause some programmer
inserts viral side effects in checked expressions,
or just wishes to start from the proof of the absence of
666 consecutive digits of e in π on the way,
then so be it.  He or she is violating the goals of
designing with the help of assertions. The goal is *not*
unrolling proven assumptions into source text, but arriving
at proven systems. So that turning off assertion checking
can be considered safe. Safe because checking will not
affect the desired effect of the program in any way that
is covered by the contract-as-agreed as being essential.

So IMHO Pre/Post/Inv are really improvements of pragma Assert.

> Another way to understand this: a contract describes states of a program.

That's not a contract. There are no parties. There is
no obligation to make predicates true on either side.
A program could define states, in the contract's space.