SPARK 2014 Rationale: Formal Containers

by Claire Dross – Nov 29, 2013

SPARK 2014 excludes data structures based on pointers. To work around this restriction, the content of a data structure can be hidden using private types. Thanks to specification functions, a model can be defined for the content of these data structures that can then be used to specify the API functions. For example, here is a SPARK 2014 specification of a linked list package using pointers. It uses a specification function Get_Model that returns the content of a linked list as an array:

package Lists is

   pragma SPARK_Mode (On);

   type Int_Array is array (Positive range <>) of Integer;
   type My_List is private;

   function Get_Model (L : My_List) return Int_Array;

   function Head (L : My_List) return Integer with
     Post => Get_Model (L) (1) = Head'Result;

   function Cons (I : Integer; L : My_List) return My_List
     with Pre  => Get_Model (L)'Last < Natural'Last,
          Post => Get_Model (Cons'Result) = I & Get_Model (L);

private
   pragma SPARK_Mode (Off);

   type My_List_Record is record
      Head : Integer;
      Tail : My_List;
   end Record;

   type My_List is access My_List_Record;

end Lists;

Instead of implementing such a linked list package herself, a user may want to use a generic container package from the library. For example, the package Ada.Containers.Doubly_Linked_Lists offers two subprograms, First_Element and Prepend, that can be used in place of Head and Cons. Unfortunately, these packages are not adapted to formal verification. In particular, cursors, that are iterators over containers, contain an internal reference to their container. As a consequence, every sub-program that modifies a container also silently modifies every cursor that references it.

As part of the SPARK 2014 development, new containers library have been introduced. Those formal containers, available under Ada.Containers.Formal_<something>, closely resemble Ada 2012 bounded containers except that cursors are not tied to a particular container and can be valid in several of them. This modification allows in particular to refer to the element designated by a given cursor Cu in a container Cont before and after a modification of Cont using the same cursor. For example, we can specify a procedure that takes a list of integers L and a cursor Cu and increments the element designated by Cu in L:

package My_Lists is new Ada.Containers.Formal_Doubly_Linked_Lists
  (Element_Type, My_Eq);

use My_Lists;

procedure Increment_Element (L : in out List; Cu : Cursor) with
  Pre  => Has_Element (L, Cu) and then Element (L, Cu) < Element_Type'Last,
  Post => Has_Element (L, Cu) and Element (L, Cu) = Element (L'Old, Cu) + 1;

Note that the specification of the procedure Increment_Element is not complete. Indeed, it does not state that the rest of the list L is not modify, that is, that it contains the same elements in the same order and that iteration can be done on L before and after the modification using the same cursors. These frame condition statement are common enough for the formal containers packages to include specific functions that facilitate their expression.

The function First_To_Previous takes a container Cont and a cursor Cu in argument and returns a container that is Cont where Cu and every cursor following it in Cont have been removed:

function First_To_Previous (Container : List; Current : Cursor) return List;

The function Current_To_Last takes a container Cont and a cursor Cu in argument and returns a container that is Cont where every cursor preceding Cu in Cont have been removed:

function Current_To_Last (Container : List; Current : Cursor) return List;

Finally, the function Strict_Equal takes two containers and returns true if and only if they contain the same elements in the same order and iteration can be done on both of them using the same cursors.

function Strict_Equal (Left, Right : List) return Boolean;

Thanks to these function, we can complete the specification of Increment_Element:

procedure Increment_Element (L : in out List; Cu : Cursor) with
  Pre  => Has_Element (L, Cu) and then Element (L, Cu) < Element_Type'Last,
  Post => Has_Element (L, Cu) and then
            Element (L, Cu) = Element (L'Old, Cu) + 1 and then
            Strict_Equal (First_To_Previous (L, Cu),
                          First_To_Previous (L'Old, Cu)) and then
            Strict_Equal (Current_To_Last (L, Next(L, Cu)),
                          Current_To_Last (L'Old, Next(L'Old, Cu)));

The implementation of Increment_Element is as simple as calling procedure Replace_Element from the formal containers' API:

procedure Increment_Element (L : in out List; Cu : Cursor) is
begin
  Replace_Element (L, Cu, Element (L, Cu) + 1);
end Increment_Element;

And guess what? GNATprove manages to prove automatically that the implementation above indeed implements the contract that we specified for Increment_Element. And that no run-time errors can be raised in this code. Not bad for a non-trivial specification!

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.