SPARK 2014 Rationale: Verifying Properties over Formal Containers

by Claire Dross – Jan 17, 2014

We saw in a previous post how we could express complex properties over formal containers using quantified expressions. In this post, I present how these properties can be verified by the proof tool called GNATprove.

A naive support for formal containers would consist in adding contracts to all subprograms in the API of formal containers, and let GNATprove analyze calls to these subprogram as it does for regular code. The problem with that approach is that, either we add lightweight contracts which don't allow proving all properties of interest, or we add heavyweight contracts that make it harder to prove properties automatically. So instead, we chose to "axiomatize" the library of formal containers, that is, we directly wrote axioms explaining to the prover how they work. This particularity is specified using a specific annotation pragma in the implementation of formal containers:

pragma Annotate (GNATprove, External_Axiomatization);

GNATprove makes some hypothesis on the function parameters used for the instantiation of a formal container. Let's see how this works on My_Sets, a set of integers defined as follows:

type Element_Type is new Integer range 1 .. 100;
function Hash (Id : Element_Type) return Hash_Type;
function Equivalent_Elements (I1, I2 : Element_Type) return Boolean;
function My_Equal (I1, I2 : Element_Type) return Boolean is (I1 = I2);
package My_Sets is new Ada.Containers.Formal_Hashed_Sets
    (Element_Type        => Element_Type,
     Hash                => Hash,
     Equivalent_Elements => Equivalent_Elements,
     "="                 => My_Equal);

Note that we do not support passing operators as actuals in a generic instantiation, so we cannot leave the default argument for the parameter "=" nor explicitly give the equality symbol "=" as an argument. We need to introduce a function wrapper My_Equal.

For GNATprove to give correct results, the arguments of the generic instantiation must respect some crucial properties:

The functions Hash, Equivalent_Elements, and My_Equal must not read or write any global.
Then, as specified in the Ada reference manual, the function Equivalent_Elements should be an equivalence relation.

GNATprove uses these properties in its proofs, so, for example, it can always prove automatically that the following properties hold for Equivalence_Elements:

--  Reflexivity
pragma Assert (for all E in Element_Type => Equivalent_Elements (E, E));
-- Symmetry
pragma Assert
  (for all E1 in Element_Type =>
     (for all E2 in Element_Type =>
          (if Equivalent_Elements (E1, E2) then Equivalent_Elements (E2, E1))));
-- Transitivity
pragma Assert
  (for all E1 in Element_Type =>
     (for all E2 in Element_Type =>
          (for all E3 in Element_Type =>
               (if Equivalent_Elements (E1, E2) and Equivalent_Elements (E2, E3) then
                       Equivalent_Elements (E1, E3)))));

Let us now see how we can prove programs using My_Sets. As an example, let us consider a function Double_All that takes a set of elements S and returns the set of all the doubles of elements of S:

--  A subtype of Set with Capacity 100.
--  The Modulus discriminant is used for the hash function.
subtype My_Set is Set (Capacity => 100, Modulus => Default_Modulus (100));
function Double_All (S : My_Set) return My_Set with
  Pre  => (for all E of S => E <= 50),
  Post => (for all E of S => Contains (Double_All'Result, 2 * E));

The precondition of function Double_All states that it is called on a set whose elements are all less than or equal to 50, using a quantified expression. Its postcondition states that the result of the function contains all the doubles of the elements of the function argument. Here is a possible implementation for Double_All:

function Double_All (S : My_Set) return My_Set is
  R       : My_Set;
  Current : Cursor := First (S);
begin
  Clear (R);
  while Has_Element (S, Current) loop
     pragma Loop_Invariant
       (Length (R) <= Length (First_To_Previous (S, Current)) 
          and then
       (for all Cu in First_To_Previous (S, Current) =>
          Contains (R, 2 * Element (S, Cu))));
     Include (R, 2 * Element (S, Current));
     Next (S, Current);
  end loop;
  return R;
end Double_All;

Note that we use a call to the procedure Clear at the beginning of the program for GNATprove to know that the set R is empty. The proof of Double_All requires a loop invariant. It states that we have already included in R the elements that appear in S before the Current cursor using the function First_To_Previous. We also need to bound the length of R to be able to prove that we do not exceed the capacity of R. Remark that we cannot prove that the length of R is equal to the number of already included elements. Indeed, since we do not know the definition of Equivalent_Elements, it could be the case that two elements of S have the same double modulo this relation.

GNATprove proves automatically that the code of Double_All cannot raise a run-time exception, and that is implements the contract of the function.

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.