Re: about the new Ada 2012 pre/post conditions

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

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? 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? Maybe there is some special
before-the-body-exceptions, propagated in some special manner? It just does
not make sense. The contract should refer to all effect of calling the
program.

> Besides, I don't understand why it is such a disaster to have precondition 
> contracts be dynamically evaluated in some cases, while it is OK to have a 
> postcondition be dynamically evaluated in some cases -- it too is a contract 
> (one that is evaluated *after* the subprogram finishes).

It is *not* OK to evaluate precondition of a program by the program itself.
It is similar to how halting becomes a problem:

procedure P is
begin
   while not HALT (P) loop
      null;
   end loop;
end P;

All this boils down to self-referential stuff.

> (Don't use specific preconditions and 
> postconditions if you care about inheritance.)

Which is a telling advise, taking into about that [true]
pre-/post-conditions is all [true] interface is about. Inheritance at the
interface level is nothing but shuffling pre-/post-conditions.

>> Another necessary contract mechanism is composition. That is when you pass
>> a downward closure to an operation, that could say: I raise what the
>> argument does. Note that this will require proper procedural types to have
>> interfaces to carry the contract with. E.g. you would be able to limit the
>> closure operation to what it is allowed to raise.
> 
> I agree with the need for composition; we had that in the never-finished 
> "global in/out" contracts. But that doesn't require "procedural types" 
> per-se;

Propagation of target contracts trough access to the target looks much more
complicated.

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