SPARK 2014 Rationale: Support for Type Invariants

by Claire Dross – Oct 12, 2016

Type invariants are used to model properties that should always hold for users of a data type but can be broken inside the data type implementation. Type invariant are part of Ada 2012 but were not supported in SPARK until SPARK Pro 17.

To demonstrate how they can be used, let us consider an implementation of binary trees as an example. As GNATprove does not support access types, we model them using indexes inside an array.

package Binary_Trees is
  type Index_Type is range 1 .. Max;
   subtype Extended_Index_Type is Index_Type'Base range 0 .. Max;
   type Position_Type is (Left, Right, Top);

   type Tree is private;

private

   type Cell is record
      Left, Right, Parent : Extended_Index_Type := 0;
      Position            : Position_Type := Top;
   end record;

   type Cell_Array is array (Index_Type) of Cell;

   type Tree is record
      Top : Extended_Index_Type := 0;
      C   : Cell_Array;
   end record;
end Binary_Trees;

Each cell contains the index of its right and left child, as well as the index of its parent. This index is 0 is the cell has no left or right child or no parent. It also contains a position which can be Top for the root of the tree and Left or Right for the other nodes, depending on whether they are left or right children in the tree structure. A tree contains an array of cells as well as the index of the tree root.

There are properties that are imposed on the record fields by the tree structure. These properties are required for a the record to represent a valid binary tree structure. For example, the root must have position Top and no parent:

(if Top /= 0 then C (Top).Parent = 0
       and then C (Top).Position = Top)

the left child of a node I must have position Left and parent I:

(for all I in Index_Type =>
         (if C (I).Left /= 0
          then C (C (I).Left).Position = Left
              and then C (C (I).Left).Parent = I))

All these properties represent an invariant over the structure. They can be grouped together in an expression function which can then be attached to the full view of Tree using a Type_Invariant aspect:

type Tree is record
      Top : Extended_Index_Type := 0;
      C   : Cell_Array;
   end record
     with Type_Invariant => Tree_Structure (Tree);

   function Tree_Structure (T : Tree) return Boolean is
     ((if T.Top /= 0 then T.C (T.Top).Parent = 0
       and then T.C (T.Top).Position = Top)
      and then
        (for all I in Index_Type =>
             (if T.C (I).Left /= 0
              then T.C (T.C (I).Left).Position = Left
                and then T.C (T.C (I).Left).Parent = I))
      and then
        ...

In spirit, this means that Tree_Structure must always return True on objects of type Tree visible from outside Binary_Trees. To ensure this property, GNATprove enforces restrictions on subprograms working on trees depending on where they are declared. If the subprogram is private, like Tree_Structure, no invariant checks are required for its parameters, neither on entry nor on exit of the subprogram. In the invariant expression, only private functions should be used so as to avoid any circularity.

If the subprogram is declared outside of Binary_Trees or if it is declared in the public part of Binary_Trees, then the invariant must hold for its input in entry of the subprogram and for its outputs in exit of the subprogram. For example, let us consider the Insert function which inserts a new node into a tree. Let us assume this is a boundary function for Tree, that is, it is declared in the public part of the specification of the package Binary_Trees in which Tree is declared:

procedure Insert (T : in out Tree; I : Index_Type; D : Direction);

The invariant is required to hold on input T when entering Insert. GNATprove will check Tree's invariant every time Insert is called inside Binary_Trees to make sure this is verified. In the same way, verification conditions are generated by GNATprove to ensure that the invariant holds for T at the end of Insert. In effect, it is like if we had written:

procedure Insert (T : in out Tree; I : Index_Type; D : Direction)with
     Pre  => Tree_Structure (T),
     Post => Tree_Structure (T);

Unlike type predicates, type invariant can be broken temporarily in the body of Insert, as long as it is restored at the end of the subprogram:

procedure Insert (T : in out Tree; I : Index_Type; D : Direction) is
      M : Model_Type := Model (T) with Ghost;
      J : Index_Type;

   begin
      --  Find an empty slot in the underlying array

      Find_Empty_Slot (T, J);

      --  Plug it as the D child of I

      T.C (J).Position := D;
      T.C (J).Parent := I;

      --  The invariant of T is broken, J is not the child of I

      if D = Left then
         T.C (I).Left := J;
      else
         T.C (I).Right := J;
      end if;

      --  Tree_Structure (T) holds again
   end Insert;

Outside of Binary_Tree, the invariant of Tree is never checked. Indeed, the rules of SPARK are enough to ensure no invariant breaking value can leak out of Binary_Tree's implementation. This allows to split considerations between multiple layers. For example, we can then reuse our binary trees to implement search trees. We do not need to prove the tree structure invariant anymore, but can simply rely on it to prove the remaining properties:

package Search_Trees with SPARK_Mode is
   type Search_Tree is private;

   function Mem (T : Search_Tree; V : Natural) return Boolean;

   procedure Insert  (T : in out Search_Tree; V : Natural; I : out Extended_Index_Type);

private

   type Value_Array is array (Index_Type) of Natural;

   type Search_Tree is record
      Struct : Binary_Trees.Tree;
      Values : Value_Array;
   end record
     with Type_Invariant => Ordered_Leafs (Search_Tree);

   function Ordered_Leafs (T : Search_Tree) return Boolean with Ghost;
end Search_Trees;

When calling Binary_Trees.Insert in the implementation of Search_Trees.Insert, GNATprove does not need to check that the invariant of T.Struct hold, as it is enforced at the boundary of Binary_Trees:

procedure Insert (T : in out Search_Tree; V : Natural; I : out Extended_Index_Type) is
   begin
      if Top (T.Struct) = 0 then
         Init (T.Struct);
         I := Top (T.Struct);
         T.Values (I) := V;
         return;
      end if;

      declare
         Current  : Extended_Index_Type := Top (T.Struct);
         Previous : Extended_Index_Type := 0;
         D        : Direction := Left;
      begin
         while Current /= 0 loop
            Previous := Current;
            if V = T.Values (Previous) then
               I := 0;
               return;
            elsif V < T.Values (Previous) then
               D := Left;
            else
               D := Right;
            end if;
            Current := Peek (T.Struct, Previous, D);
         end loop;

         --  We have found the leaf where we want to insert V

         Insert (T.Struct, Previous, D);
         --  No invariant check
         --  The tree structure is preserved by Insert

         I := Peek (T.Struct, Previous, D);
         T.Values (I) := V;

         --  Check that the leaf ordering is preserved
      end;
   end Insert;

Note that GNATprove does not support type invariants on tagged types nor on types declared in nested/child units for now. Therefore, we can neither change Search_Tree to derive from Tree nor move Binary_Trees as a nested or child package of Search_Trees.

Posted in #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.