Ada Conformity Assessment Authority      Home Conformity Assessment   Test Suite ARGAda Standard
Overview of Ada 2022
Jeff Cousins
Contents   Index   Search   Previous   Next 

3.7 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;
   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.

Contents   Index   Search   Previous   Next 
© 2021, 2022 Jeff Cousins