SPARK 2014 Rationale: Functional Update

by Yannick Moy – Jan 21, 2015

As mentioned in a previous post, attribute Old allows expressing inside a postcondition the value of an object at subprogram entry. For example, the postcondition of the procedure Incr can be written:

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

This is fine for a scalar variable, but what about a composite variable? If X is a record with 3 integer components A, B and C, we may write:

procedure Incr (X : in out Rec) with
  Post => X.A = X.A'Old + 1;

and if X is an array of integers, we may write:

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

This is fine for specifying the value of the record component or array element which has been incremented, but what about others? As humans, we may read implicitly in the contracts above that components other than A, and elements other than at index 1, have not been modified by calling Incr. But the analysis tool GNATprove cannot rely on that implicit information, as the same contracts may be correct for procedures that do modify components B and C and elements at indexes different from 1. Hence, GNATprove interprets the contracts above as:

X is an "in out" parameter that can be modified by calling Incr, and the only thing we know about that is how the value of component A (or the element at index 1) is modified. We don't know anything about how other components (or elements) are modified.

The solution is to express explicitly in the postcondition the property that other components or elements are not modified by Incr:

procedure Incr (X : in out Rec) with
  Post => X.A = X.A'Old + 1 and then
          X.B = X.B'Old and then
          X.C = X.C'Old;

procedure Incr (X : in out Arr) with
  Post => X(1) = X(1)'Old + 1 and then
          (for all J in X'Range => (if J /= 1 then X(J) = X'Old(J)));

With these postconditions, GNATprove can use the fact that only component A and the element at index 1 are modified by calling Incr, when analyzing Incr's callers.

But the above postconditions are not so easy to read, and scale poorly if there are many more components, or if the modification is applied to a deeply nested component. This is why SPARK defines a special attribute Update which copies the value of a composite object (record or array) with some modifications. The above postconditions can be expressed equivalently:

procedure Incr (X : in out Rec) with
  Post => X = X'Old'Update (A => X.A'Old + 1);

procedure Incr (X : in out Arr) with
  Post => X = X'Old'Update (1 => X(1)'Old + 1);

This attribute is equivalent to the square bracket notation used in Ada 2005 for the same purpose. It can also be used with benefits to express functions whose only purpose is to return a slightly modified version of their input. For example (using the syntax of expression functions):

function Incr (X : Rec) return Rec is (X'Update (A => X.A + 1));

function Incr (X : Arr) return Arr is (X'Update (1 => X(1) + 1));

Such usage is quite common in functional languages. For example both OCaml and Haskell have a special syntax for functional record update.

To know more about the attribute Update, see SPARK User's Guide and SPARK Reference Manual.

Posted in #Language #Formal Verification #SPARK

About 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.