Rationale for Ada 2012

John Barnes
Contents   Index   References   Search   Previous   Next 

9.3.5 Pre/post-conditions for subprograms

The original proposal was to add pragmas such as Pre_Assert and Post_Assert. Thus in the case of a subprogram Push 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));
This was all abandoned in Ada 2005 for various reasons; one being that pragmas are ugly for such an important matter.
However, this is neatly solved in Ada 2012 by the introduction of aspect specifications so we can now write
procedure Push(S: in out Stack; X: in Item)
      Pre => not Is_Full(S),
      Post => not Is_Empty(S);
which is really excellent; this is discussed in detail in chapter 2, “Contracts and aspects”.

Contents   Index   References   Search   Previous   Next 
© 2011, 2012, 2013 John Barnes Informatics.
Sponsored in part by:
The Ada Resource Association:


and   Ada-Europe: