SPARK 2014 Rationale: Expressing Properties over Formal Containers

by Claire Dross – Dec 13, 2013

We saw in a previous post how formal containers can be used in SPARK code. In this post, I describe how to express properties over the content of these containers, using quantified expressions. In their simplest form, quantified expressions in Ada 2012 can be used to express a property over a scalar range. For example, that all integers between 1 and 6 have a square less than 40:

(for all J in 1 .. 6 => J * J < 40)

or that every even integer greater than 2 can be expressed as the sum of two primes (also known as Goldbach's conjecture):

(for all J in Integer =>
  (if J > 2 then
    (for some P in 1 .. J / 2 => Is_Prime (P) and then Is_Prime (J - P))))

The second form of quantified expressions allows to express a property over a standard container. For example, that all elements of a list of integers are prime, which can be expressed by iterating over cursors as follows:

(for all Cu in My_List => Is_Prime (Element (Cu)))

The general mechanism in Ada 2012 that provides this functionality relies on the use of tagged types (for the container type) and various aspects involving access types so cannot be applied to the SPARK formal containers.

Instead, we have defined in GNAT an aspect Iterable that provides the same functionality in a simpler way, leading also to much simpler object code. For example, here is how it can be used on a type Container_Type:

type Container_Type is ... --  the structure on which we want to quantify
  with Iterable => (First       => My_First,
                    Has_Element => My_Has_Element,
                    Next        => My_Next);

where My_First is a function taking a single argument of type Container_Type and returning a cursor:

function My_First (Cont : Container_Type) return My_Cursor_Type;

and My_Has_Element is a function taking a container and a cursor and returning whether this cursor has an associated element in the container:

function My_Has_Element (Cont : Container_Type; Pos : My_Cursor_Type) return Boolean;

and My_Next is a function taking a container and a cursor and returning the next cursor in this container:

function My_Next (Cont : Container_Type; Pos : My_Cursor_Type) return My_Cursor_Type;

Now, if the type of object Cont is iterable in the sense given above, it is possible to express a property over all elements in Cont as follows:

(for all Cu in Cont => Property (Cu))

The compiler will generate code that iterates over Cont using the functions My_First, My_Has_Element and My_Next given in the Iterable aspect, so that the above is equivalent to:

declare
   Cu     : My_Cursor_Type := My_First (Cont);
   Result : Boolean := True;
begin
   while Result and then My_Has_Element (Cont, Cu) loop
      Result := Result and Property (Cu);
      Cu     := My_Next (Cont, Cu);
   end loop;
end;

where Result is the value of the quantified expression.

We have used the Iterable aspect to provide quantification for formal containers, using the functions First, Has_Element and Next of the formal containers' API. For example, the definition of formal doubly linked lists looks like:

type List (Capacity : Count_Type) is private with
   Iterable => (First       => First,
                Next        => Next,
                Has_Element => Has_Element);

This allows a user to specify easily the contract of a function that searches for the first occurrence of 0 in a doubly linked list, using here contract cases:

function Search (L : List) return Cursor with
  Contract_Cases =>
    --  first case: 0 not in the list
    ((for all Cu in L => Element (L, Cu) /= 0) =>
        Search'Result = No_Element,
    --  second case: 0 is in the list
     (for some Cu in L => Element (L, Cu) = 0) =>
        Element (L, Search'Result) = 0
          and then
        (for all Cu in First_To_Previous (L, Search'Result) => Element (L, Cu) /= 0));

The first case specifies that, when the input list does not contain the value 0, then the result is the special cursor No_Element. The second case specifies that, when the input list contains the value 0, then the result is the first cursor in the list that has this value.

Posted in #Language #Formal Verification #SPARK

About Claire Dross

Claire Dross has a PhD in deductive verification of programs using a satisfiability modulo theory solver with the Universite Paris-Sud. She also has an engineering degree from the Ecole Polytechnique and an engineering degree from the Ecole Nationale Superieure des Telecommunications. At AdaCore, she works full-time on the formal verification SPARK 2014 toolset.