Re: about the new Ada 2012 pre/post conditions

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

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.
Therefore it cannot depend on the program state.

Another way to understand this: a contract describes states of a program.
As such it cannot depend on them.

Yet another way: the language of contracts is not the object language:

http://en.wikipedia.org/wiki/Object_language

> But that's never, ever been true in Ada.

I already said that type constraints are not contracts. E.g. an actual
value of the discriminant does not create a new contract. The contract
covers *all* possible values of the discriminant.

> Exactly. You claim that there cannot be such a thing as a dynamically 
> enforced contract.

Absolutely. How could you enforce a contract which has been *already*
violated? If a program reaches an illegal state, it is in that state.
Period.

> But handling exceptions raised for contracts does not make the program any 
> less wrong;

Really? What is the purpose of the exercise? Raising exception, rolling the
stack, finalizing stuff, and so on only to resign that the program is as
wrong as it was before? (Maybe it is even *more* wrong than it was? (:-))

>>> The only kind of correctness checks that *can* exist in general are dynamic.
>>> Ada's entire reason to exist is to include checks like range checks and
>>> overflow checks to programs. Without them you get the buffer overflows 
>>> and other errors that plague C code.
>>
>> Yes, but irrelevant. These checks are not contract checks, because,
>> otherwise you are in contradiction. No words can change that.
> 
> Certainly not if you insist on using an unnecessarily limiting definition of 
> "contract".

Yes, the contract as opposed to the implementation limits the former not to
be the latter [POV #2]. But I am all open to accept that Eiffelesque/Ada
2012 "contracts" are implementations [POV #1]. Do you?

>> But also there are important consequences for software engineering. Since
>> these checks have nothing to do with contracts, they must be considered as
>> a part of the program semantics and all possible outcomes must be
>> *handled*. The problem of buffer overflow is exactly in pretending that it
>> cannot overflow. So the program is broken when it does.
> 
> That's certainly a fallacy in general. Most Ada programs are best off *not* 
> handling exceptions caused by outright bugs,

What about the statement: "Most Ada programs are best off not adding
integer numbers caused by outright bugs"?

The actual fallacy is in pretending that a bug can be handled. You can
handle/be in only anticipated states.

The proper statement should have been: "Ada is best to make the programmer
aware of the states he might overlooked."

>>> I suppose you have a totally different definition of "correctness checks"
>>> than I do; as usual, we can't have a useful discussion because you have 
>>> your own set of terminology.
>>
>> Terminology is secondary to the semantics. The problem is with the 
>> meaning.
> 
> Right. I recall in the past that you've been unwilling to grasp the idea of 
> bugs being detected at runtime.

Sure, because that is rubbish, and always was:

http://en.wikipedia.org/wiki/Liar_paradox

> [As an aside, this means you do not want real exception contracts, since 
> they cannot usefully be done without having it be implementation-defined 
> when an exception is raised by a predefined check. The canonical semantics 
> of Ada would require assuming that every line raises Storage_Error, 
> Program_Error, and usually Constraint_Error -- that would make it virtually 
> impossible to eliminate those exceptions from contracts.

I don't see it as a big problem. There is a difference between an
obligation to raise exception and a possibility that an exception could be
raised.

The contract language should deploy the intuitionistic logic. That is
necessary anyway because some things are not provable. In the
intuitionistic logic A or not A is not true (no law of excluded middle).
E.g.

   "raise E"   (I will raise E)

and

   not "not raise E"   (I may raise E. I don't promise not to rase E)

are not equivalent statements.

The vendors could gradually reduce the number of cases where E may be
raised without making clients relying on weaker contracts illegal. The
second cannot be misused to prove that E is raised. It just does not follow
from the second, and conversely.

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