AdaCore Blog

GNATprove Tips and Tricks: Referring to Input in Contracts

by Yannick Moy

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

procedure Extract (A : in out My_Array; J : Integer; V : out Value) with
  Post => (if J in A'Range then V = A(J)'Old and A(J) = 0);  --  INCORRECT

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: prefix that is potentially unevaluated must denote an entity

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

procedure Extract (A : in out My_Array; J : Integer; V : out Value) with
  Post => (if J in A'Range then V = A'Old(J) and A(J) = 0);  --  CORRECT

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:

procedure Extract (A : in out My_Array; J : Integer; V : out Value) with
  Contract_Cases => ((J in A'Range) => V = A(J)'Old and A(J) = 0,
                     others         => True);

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):

procedure Extract (A : in out My_Array; J : Integer; V : out Value) with
  Contract_Cases => ((J in A'Range) =>
                       (for all K in 1 .. J =>
                          (Condition(A(K)) or else V = Get(A)'Old(K))),
                     others         => True);

In such a case, the compiler does not issue an error (contrary to what it does in postconditions), instead it issues a warning: warning: prefix of attribute "Old" is always evaluated when related consequence is selected

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!

Posted in #Language    #Formal Verification    #SPARK   

About Yannick Moy

Yannick Moy is a Senior Software Engineer at AdaCore and co-director of the ProofInUse joint laboratory. At AdaCore, he works on software source code analyzers CodePeer and SPARK, aiming either at detecting bugs or at verifying safety/security properties. Yannick leads the developments of SPARK, a product he presents in articles, conferences, classes and blogs (in particular Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.