AdaCore Blog

SPARK 2014 Rationale: Pre-call and Pre-loop Values

by Yannick Moy –

Subprogram contracts are commonly presented as special assertions: the precondition is an assertion checked at subprogram entry, while the postcondition is an assertion checked at subprogram exit. A subtlety not covered by this simplified presentation is that postconditions are really two-state assertions: they assert properties over values at subprogram exit and values at subprogram entry.

Take the very simple example of a procedure Increment:

procedure Increment (X : in out Integer) with
  Post => X = X'Old + 1;

The postcondition of Increment states that the value of X at subprogram exit, denoted X, is one above the value of X at subprogram entry, denoted X'Old. We're using a special attribute Old in SPARK 2014 (and in Ada 2012) to denote the value of an object at subprogram entry. By using X'Old in the postcondition, we instruct the compiler to create a copy of X at subprogram entry, that can be dynamically tested when exiting the subprogram to check that the postcondition holds.

This special attribute has many equivalent constructs in other languages:

Like most its counterparts, the Old attribute can only be used in postconditions (and consequence expressions in contract cases, that have the same scope as postconditions). But in Ada 2012, its use was restricted to avoid a common pitfall found in all other languages.

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 value of A(J) at subprogram entry is only meaningful if J is in the bounds of A. If we allowed the code above, then a copy of A(J) would 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:

example.ads:5:44: 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

For formal verification with SPARK 2014, the attribute Old is not sufficient: the postcondition is not the only two-state assertion, loop invariants (special assertions used by the formal verification tool to summarize the effect of a loop) have the same property that they need to relate the state of the program before the loop starts, and the state of the program after a given number of loop iterations. The attribute Loop_Entry was added in SPARK 2014 for that purpose.

Take the example of a procedure Increment_N, which calls N times the previous procedure Increment:

procedure Increment_N (X : in out Integer; N : Positive) is
begin
   for J in 1 .. N loop
      Increment (X);
      pragma Loop_Invariant (X = X'Loop_Entry + J);
   end loop;
end Increment_N;

The loop invariant expresses that the value of X after the J'th iteration is the initial value of X at loop entry, denoted X'Loop_Entry, plus J. With this loop invariant, the formal verification tool GNATprove is able to prove that the contract of Increment_N is fulfilled

procedure Increment_N (X : in out Integer; N : Positive) with
  Post => X = X'Old + N;

To avoid similar pitfalls as the one mentioned above for attribute Old, attribute Loop_Entry is similarly restricted in expressions that are potentially unevaluated, and it can only be used in assertions, loop invariants and loop variants in the top-level list of statements in a loop.

Note that Old and Loop_Entry do not apply to any expression like (X + Y), but only to name expressions (in Ada grammar), such as a component selection X.C'Old, a dereference X.all'Old, a call F(X,Y,Z)'Old, etc.

For more details on the use of attributes Old and Loop_Entry, see:

Posted in #Formal Verification    #SPARK   

About Yannick Moy

Yannick Moy

Yannick Moy is Head of the Static Analysis Unit at AdaCore. Yannick contributes to the development of SPARK, a software source code analyzer aiming at verifying safety/security properties of programs. He frequently talks about SPARK in articles, conferences, classes and blogs (in particular blog.adacore.com). Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.