As discussed in a previous post about pre-call values, the Old attribute can be used in postconditions to refer to the value of an object prior to calling the subprogram. As the compilation of this expression involves a copy of the object on entry to the subprogram, the compiler automatically detects cases which could induce the programmer into thinking that it is not evaluated, while at run time this evaluation could fail (say, by failing a language check).

Take the example of a procedure Extract, which copies the value of array A at index J in parameter V, and zeroes out this value in the array, but only if J is in the bounds of A

Clearly, the intent of the programmer here is that the value of A(J) is evaluated only if J is in the bounds of A. But that's not how this code is compiled according to Ada rules. If the code above was allowed, then a copy of A(J) would always be made on entry to subprogram Extract, even when J is out of bounds, which would raise a run-time error. Therefore, use of Old in expressions that are potentially unevaluated (like the then-part in an if-expression, or the right argument of a shortcut boolean expression) is restricted to plain variables: A is allowed, but not A(J). The GNAT compiler issues the following error on the code above:

The correct way to specify the postcondition in that case is:

The problem is more subtle when the contract of a subprogram is specified using contract cases. Indeed, each case will correspond to a subset of the executions only, so applying the same rule as for postconditions would forbid completely the use of attribute Old in contract cases.

For example, we might want to express the contract of procedure Extract by using cases:

In fact, the above is valid, because the rule is that only those objects used as prefixes of an attribute Old in the currently enabled case are copied on entry to the subprogram. So if Extract is called with J out of the range of A, then the second case is enabled, so A(J) is not copied when entering procedure Extract.

It may still be the case that some complex contracts require referring to the value of complex objects at subprogram entry, in particular when getter functions are involved.

For example, the contract of procedure Extract may specify that, when J in is in the range of A, then for all values K in some range, then either a condition holds or the value of V is equal to some expression involving attribute Old applied to a call to a getter function (using here a shortcut boolean expression):

In such a case, the compiler does not issue an error (contrary to what it does in postconditions), instead it issues a warning:

It is then up to the user to decide if this warning uncovers a potential problem. If not, the user can silence the compiler with a suitable pragma Warnings Off. The good news for formal verification with GNATprove is that complex contracts that would not be allowed as postconditions can be expressed using contract cases!