Rationale for Ada 2012

John Barnes

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)
   with
      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”.