Other support for pre- and postconditions

Pre/Post for access-to-subprogram types (AI12-0220) allows Pre and Post aspects for access-to-subprogram types, so that contract information is available when calling a subprogram indirectly via an access value, as well as (or even instead of) when called directly. For example, to check that a parameter is even:

type T1 is access procedure (X : Integer)
   with Pre => X mod 2 = 0;
procedure Foo (X : Integer) is ... end;
...
   Ptr1 : T1 := Foo'Access;
begin
   Ptr1.all (222); -- Precondition check performed

Making 'Old more flexible (AI12-0280-2). Currently the following is illegal as the A.all in A.all'Old is “potentially unevaluated”:

procedure Proc (A : access Integer)
with Post =>
(if A /= null then (A.all'Old > 1 and A.all > 1));

This is now relaxed. Thinking less of what it may not be possible to evaluate, but more of what can be evaluated in advance, the term “known on entry” is introduced to cover such expressions (the most obvious example being a static expression), and if it is possible to tell on entry to a subprogram that an X'Old need not be evaluated then it isn't. In the example, A is an in parameter of an elementary type (which includes access types) so it is passed by copy and cannot change, so if A is null on entry then A.all'Old would not be evaluated.

3.7 Other support for pre- and postconditions