Re: about the new Ada 2012 pre/post conditions

["Randy Brukardt" <randy@rrsoftware.com>]

"Nasser M. Abbasi" <nma@12000.org> wrote in message 
news:jrsjr7$uuo$1@speranza.aioe.org...
...
> -----------------------------
> pragma Assertion_Policy(Check);
>
> procedure Push(S: in out Stack; X: in Item)
>   with
>     Pre => not Is_Full(S),
>     Post => not is Empty(S);
>   is
>     ....
> end Push;
> ---------------------
>
> One thing to notice right away, is that the pre/post checks
> can be disabled or enabled by the pragma.

Yes, but this is not a problem if you are careful. Specifically, your 
packages should at least contain

   pragma Assertion_Policy (Pre => Check,
                                           Pre'Class => Check,
                                           Static_Predicate => Check,
                                           Dynamic_Predicate => Check);

(That is, all of the "inbound" assertion checks.)

Then, the only way for someone to ignore these checks is to edit the source 
code of your library. If they do that, they've clearly "violated the 
warranty", and you have no obligation to make the body do anything useful if 
they do that.
[Aside: note that assertions are "ignored", not "suppressed". The difference 
is that suppressed checks can still be made; it is only a permission to the 
compiler, not a requirement; ignored checks cannot be made.]

This was a major topic of the Texas ARG meeting (the last one mainly about 
Ada 2012), and the above is the solution that we came up with. Note that 
there was a *lot* of discussion and opinion on this topic. Some people felt 
that any time someone ignores checks, that the program is erroneous and 
there ought to be no expectation that it works (if the checks would fail). 
Others (including me) felt that adding erroneous behavior because you added 
something that was supposed to make the program safer was nonsensical.

...
> So, what is one to do? use pre/post AND also add
> an extra check for full stack in the code as before?
> does not make sense.

Do as above. Force "inbound" checks to always be on (there is no need to 
leave "post" and "invariant" on, they only can fail due to a bug in your own 
code, not by anything that the caller can do).

                                    Randy.