Re: about the new Ada 2012 pre/post conditions

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

On Wed, 4 Jul 2012 20:45:20 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:a555h2psfssb$.1be3awg0xbewa.dlg@40tude.net...
>> On Tue, 3 Jul 2012 00:28:31 -0500, Randy Brukardt wrote:
>>
>>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>>> news:xmybo646240w$.13rwa9qwsliyp$.dlg@40tude.net...
>>>> On Tue, 26 Jun 2012 13:50:28 +0200, stefan-lucks@see-the.signature 
>>>> wrote:
>>> ...
>>>> They are contracts when checked statically and implementations when
>>>> checked dynamically.
>>>
>>> No, they're always contracts. They certainly aren't "implementation",
>>> because they do *not* belong to the subprogram; they're checked *before* 
>>> the subprogram is called.
>>
>> Checked by whom?
> 
> By the caller, not the called body.
>
>> How does this make any difference to the caller or to the
>> program as a whole? Is there a way to determine whether an exception was
>> raised in the body or "before" the body?
> 
> Sure: you can handle an exception raised in the body in the body itself; you 
> cannot handle an exception raised by the call in the body.

That is irrelevant to the question asked. It was about the CALLER. Whatever
happening on the other side is an implementation. You cannot avoid #1 or
#2.

>> Maybe there is some special
>> before-the-body-exceptions, propagated in some special manner? It just 
>> does not make sense.
> 
> It's been that way in Ada since at least Ada 80 -- exceptions raised by the 
> call cannot be handled in the body, exceptions raised in the body can be 
> handled in the body. Amazing to find out that the model "does not make 
> sense" after 30+ years. ;-) It has never been the case that constraint 
> failures are part of the effect of the subprogram; they're part of the 
> effect of the call (and thus belong to the caller, not the callee).

All effects always belong to the caller. Whatever the caller does is to
obtain these effects.

>> The contract should refer to all effect of calling the program.
> 
> It does. The call itself is not part of the effect of "calling the 
> subprogram".

Then the contract does not cover all effects of putting a call statement
into an Ada program.

The same question again: on the language level, what a sequence of
characters denoting call to the subprogram P is supposed to *mean*? The
effect of writing, compiling, running programs containing that refer to P
is what?

Putting it even simpler. What is the effect of:

   sqrt (-1.0)

No effect? Any effect?

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