Rationale for Ada 2005
9.3.5 Pre/post-conditions for subprograms
This proposal (AI-288
was to add pragmas such as Pre_Assert
. Thus in the case of a subprogram
on a type Stack
we might write
procedure Push(S: in out Stack; X: in Item);
pragma Pre_Assert(Push, not Is_Full(S));
pragma Post_Assert(Push, not Is_Empty(S));
These pragmas would be controlled by the pragma Assertion_Policy
which controls the pragma Assert (which was
of course incorporated into Ada 2005). Optional message parameters were
allowed as well.
The general idea was that when the procedure Push
was called, the expression Is_Full(S) would
be evaluated and if this were false then action would be taken as for
an Assert pragma. Note that the key difference
from assert is that the pragmas go on the subprogram specification whereas
to use Assert it would have to be placed in
There were other pragmas for dispatching subprograms
and so this was not quite so simple as at first appeared.
The proposal was abandoned for a number of reasons.
There were more important matters to deal with and we were running out
of time. Moreover, it seemed just the sort of topic where user experience
on a trial implementation would be helpful in deciding what was required.
And there was some feeling that since this was all dynamic it was not
helpful to the high integrity community where the emphasis was on static
analysis and proof.
© 2005, 2006, 2007 John Barnes Informatics.
Sponsored in part by: