Re: about the new Ada 2012 pre/post conditions

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

On Thu, 21 Jun 2012 15:32:21 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:npdjip6ohqlt$.1x6bxc9jsaago$.dlg@40tude.net...
> ...
>> This is what constitutes the core inconsistency about dynamic
>> pre-/post-conditions. If they #1 implement behavior (e.g the stack contract
>> to raise something when full), then they cannot be suppressed and do not
>> describe the contract. If they do describe the contract #2, they may not
>> implement it and thus shall have no run-time effect.
> 
> You're right, but I don't see any inconsistency. They are clearly #1, and 
> that includes all of the existing Ada checks as well.

If you take a stance on #1, then checking stack full is no more evaluation
of the precondition, which does not depend on the stack state anymore, as
it of course should be. So the "true" precondition is just: True. Then why
on earth anybody would denote it as:

   Pre => not Is_Full (S)

And implementations leaking into declarations is certainly a very bad idea.
An even worse idea is to slice implementations into parts of unclear
purpose. Instead of one package body, the maintainer will have to inspect
the body, and so-.called pre-/post-conditions slices.

Neither #1 nor #2 is defendable.

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