Program verification in SPARK - Counting elements in an array

Question

I wrote a very simple program but I failed to prove it's functional correctness. It uses a list of items, with each item having a field indicating if it's free or used :

   type t_item is record
      used  : boolean := false; 
      value : integer   := 0;
   end record;

   type t_item_list is array (1 .. MAX_ITEM) of t_item;
   items       : t_item_list;

There is also a counter indicating the number of used elements :

  used_items  : integer   := 0;

The append_item procedure checks the used_items counter to see if the list is full. If it's not, the first free entry is marked as used and the used_items counter is incremented :

   procedure append_item (value : in  integer; success : out boolean)
   is
   begin

      if used_items = MAX_ITEM then
         success := false;
         return;
      end if;

      for i in items'range loop
         if not items(i).used then
            items(i).value := value;
            items(i).used  := true;
            used_items     := used_items + 1;
            success := true;
            return;
         end if;
      end loop;

      -- Should be unreachable
      raise program_error;
   end append_item;

I don't know how to prove that used_items equals the number of used elements in the list. Note also that gnatprove messages sometimes are puzzling and I don't know where to look for some more informations in the many gnatprove/* files. In fact, the main difficulty for me is to figure out what the prover needs. I would be very glad if you have some indications about all that.

Answer 1

This version was quite a bit more work , and probably can be improved upon, but it attempts to prove more functional properties one might want to apply to this problem. For example, it ensures that adding an element to the list only modifies one storage element, without modifying others, and that the number of elements in the list matches the number of used slots in the array. This version also provides a main program which is written in SPARK that uses the package.

I did have an intermediate version which I arrived at fairly easily that proved the extra functional requirements, but when I tried to use it with a client program written in SPARK, it led me to add to and revise what I had.

package Array_Item_Lists with SPARK_Mode is

   Max_Item : constant := 3; -- Set to whatever limit is desired

   subtype Element_Count is Natural range 0 .. Max_Item;
   subtype Element_Index is Natural range 1 .. Max_Item;

   type Integer_List is private;

   function Create return Integer_List
     with Post => Length (Create'Result) = 0
       and then Used_Count (Create'Result) = 0
       and then not Is_Full (Create'Result)
       and then Not_Full (Create'Result)
       and then (for all I in 1 .. Max_Item =>
                   not Has_Element (Create'Result, I));

   function Length (List : Integer_List) return Element_Count;
   function Used_Count (List : Integer_List) return Element_Count;

   --  Is_Full is based on Length being = Max_Item
   function Is_Full (List : Integer_List) return Boolean;

   --  Not_Full is based on there being empty slots in the list available
   --  Since the length is kept in sync with number of used slots, the
   --  negation of one result should be equivalent to the result of the other 
   function Not_Full (List : Integer_List) return Boolean;

   function Next_Index (List : Integer_List) return Element_Index
     with Pre => Used_Count (List) = Length (List)
     and then Length (List) < Max_Item and then Not_Full (List),
          Post => not Has_Element (List, Next_Index'Result);

   function Element (List  : Integer_List;
                     Index : Element_Index) return Integer;

   function Has_Element (List  : Integer_List;
                         Index : Element_Index) return Boolean;

   procedure Append_Item (List    : in out Integer_List;
                          Value   : Integer;
                          Success : out Boolean)
   with
     Pre  => Used_Count (List) = Length (List)
        and then (if Length (List) < Max_Item
                   then Not_Full (List) and then
                     not Has_Element (List, Next_Index (List))
                 else Is_Full (List)),
     Post =>
       (if not Is_Full (List) then Not_Full (List)) and then
         (if Length (List'Old) < Max_Item
                  then Success
          and then Length (List) = Length (List'Old) + 1
          and then Element (List, Next_Index (List'Old)) = Value
          and then Has_Element (List, Next_Index (List'Old))
          and then (for all I in 1 .. Max_Item =>
                      (if I /= Next_Index (List'Old) then
                           Element (List'Old, I) = Element (List, I)
                       and then
                         Has_Element (List'Old, I) = Has_Element (List, I)))
          and then Used_Count (List) = Used_Count (List'Old) + 1

           else not Success and then
                Length (List) = Max_Item and then List'Old = List
         and then Used_Count (List) = Max_Item);

private

   type t_item is record
      Used  : Boolean := False; 
      Value : Integer   := 0;
   end record;

   type t_item_list is
     array (Element_Count range 1 .. Element_Count'Last) of t_item;

   type Integer_List is
      record
         Items      : t_item_list := (others => (Used => False, Value => 0));
         Used_Items : Element_Count := 0;
      end record;

   function Element (List  : Integer_List;
                     Index : Element_Index) return Integer is
     (List.Items (Index).Value);

   function Has_Element (List  : Integer_List;
                         Index : Element_Index) return Boolean is
      (List.Items (Index).Used);

   function Length (List : Integer_List) return Element_Count is
      (List.Used_Items);

   function Is_Full (List : Integer_List) return Boolean is
     (for all Item of List.Items => Item.Used
      and then Length (List) = Max_Item);

   function Not_Full (List : Integer_List) return Boolean is
     (for some Item of List.Items => not Item.Used
      --  Used_Count (List) < Max_Item
     );

end Array_Item_Lists;

I'm not quite happy about having both an Is_Full function and a Not_Full function, and that may be something that can be simplified. But I did manage to get this to prove, once I added some reasonable assumptions in the body below.

pragma Ada_2012;
package body Array_Item_Lists with SPARK_Mode is

   procedure Append_Item (List    : in out Integer_List;
                          Value   :        Integer;
                          Success : out    Boolean)
   is
      Old_Used_Count : constant Element_Count := Used_Count (List);
   begin

      if List.Used_Items = Max_Item then
         Success := False;
         return;
      end if;

      declare
         Update_Index : constant Element_Index := Next_Index (List);
      begin

         pragma Assert (List.Items (Update_Index).Used = False);

         List.Items (Update_Index) := (Value => Value, Used => True);
         List.Used_Items     := List.Used_Items + 1;
         Success := True;
         pragma Assert (List.Items (Update_Index).Used = True);

         --  We have proven that one the one element of the array
         --  has been modified, and that it was previous not used,
         --  and that not it is used. From this, we can now assume that
         --  the use count was incremented by one
         pragma Assume (Used_Count (List) = Old_Used_Count + 1);

         --  If the length isn't full (Is_Full) we can assume the
         --  number of used items has room also. We incremented both
         --  of these above, and the two numbers are always in sync.
         pragma Assume (if not Is_Full (List) then Not_Full (List));

      end;

   end Append_Item;

   -----------------------------------------------------------------

   function Create return Integer_List is
      Result : Integer_List := (Items => <>,
                                Used_Items => 0);
   begin

      for I in Result.Items'Range loop         
         Result.Items (I) := (Used => False, Value => 0);

         pragma Loop_Invariant
           (for all J in 1 .. I => Result.Items (J).Used = False);

      end loop;

      pragma Assert (for all Item of Result.Items => Item.Used = False);

      --  Since we have just proven that all items are not used, we know
      --  the Used_Count has to be zero, and hence we are not full
      --  so we can make the following assumptions
      pragma Assume (Used_Count (Result) = 0);
      pragma Assume (Not_Full (Result));

      return Result;
   end Create;

   -----------------------------------------------------------------

   function Next_Index (List : Integer_List) return Element_Index
   is
      Result : Element_Index := 1;
   begin

      Search_Loop :
      for I in List.Items'Range loop

         pragma Loop_Invariant
            (for some J in I .. Max_Item => not List.Items (J).Used);

         if not List.Items (I).Used then
            Result := I;
            exit Search_Loop;
         end if;
      end loop Search_Loop;

      return Result;
   end Next_Index;

   function Used_Count (List : Integer_List) return Element_Count is
      Count : Element_Count := 0;
   begin
      for Item of List.Items loop
         if Item.Used then
            Count := Count + 1;
         end if;
      end loop;

      return Count;
   end Used_Count;

end Array_Item_Lists;

And finally, here is a SPARK main program that makes calls to the above package

with Ada.Text_IO; use Ada.Text_IO;
with Array_Item_Lists;

procedure Main with SPARK_Mode
is
   List : Array_Item_Lists.Integer_List := Array_Item_Lists.Create;
   Success : Boolean;
begin

   Array_Item_Lists.Append_Item (List    => List,
                                 Value   => 3,
                                 Success => Success);

   pragma Assert (Success);

   Array_Item_Lists.Append_Item (List    => List,
                                 Value   => 4,
                                 Success => Success);

   pragma Assert (Success);

   Array_Item_Lists.Append_Item (List    => List,
                                 Value   => 5,
                                 Success => Success);

   pragma Assert (Success);

   Array_Item_Lists.Append_Item (List    => List,
                                 Value   => 6,
                                 Success => Success);

   pragma Assert (not Success);

   Put_Line ("List " &
             (if Array_Item_Lists.Is_Full (List)
                then "is Full!" else "has room!"));
end Main;

Answer 2

I liked Simons approach, it was close to working I think.

I used that as a starting point, and applied some changes which I was able to prove using SPARK community edition, without needing additional support packages.

One of the first things I did was to take advantage of Ada's stronger typing to constrain the types as much as possible. In particular, rather than defining Used_Items as an Integer, I defined an Element_Count subtype whose range cannot exceed Max_Items. The more you can apply such constraints, the less work you need to pass on to the prover.

I then created an Integer_List type as a higher level abstraction type, and moved the array types and element types into the private part of the package.

Doing this, I found simplified the interface, I think. As it then made sense to create helper functions (Length and Is_Full) which are used in the preconditions to more simply express the properties to the client, which helps because they are repeated several times in the pre and post conditions, but which are expanded in the private part of the package to more specifically provide the detail. I used conditional expressions in the pre and post conditions, as I think that more clearly expresses the contract to the reader.

The only other thing I found I needed to add was a loop invariant in the body of the Append_Item. The prover told me that I was missing a loop invariant, which I added. You basically need to prove that you cannot exit the loop without falling into the if statement finding a slot to add the new value.

package Array_Item_Lists with SPARK_Mode is

   Max_Item : constant := 3;

   subtype Element_Count is Natural range 0 .. Max_Item;

   type Integer_List is private;

   function Length (List : Integer_List) return Element_Count;

   function Is_Full (List : Integer_List) return Boolean;

   procedure Append_Item (List    : in out Integer_List;
                          Value   : Integer;
                          Success : out Boolean)
     with
       Pre  => (if Length (List) < Max_Item
                      then not Is_Full (List)
                      else Is_Full (List)),
       Post =>
             (if Length (List'Old) < Max_Item
              then Length (List) = Length (List'Old) + 1
              and then Success 
             else (Length (List'Old) = Max_Item and then Success = False));

private

   type t_item is record
      used  : Boolean := False; 
      value : Integer   := 0;
   end record;

   type t_item_list is
     array (Element_Count range 1 .. Element_Count'Last) of t_item;

   type Integer_List is
      record
         Items : t_item_list;
         used_items : Element_Count := 0;
      end record;

   function Length (List : Integer_List) return Element_Count is
      (List.used_items);

   function Is_Full (List : Integer_List) return Boolean is
      (for all Item of List.Items => Item.used);

end Array_Item_Lists;


pragma Ada_2012;
package body Array_Item_Lists with SPARK_Mode is

   procedure Append_Item (List    : in out Integer_List;
                          Value   : Integer;
                          Success : out Boolean) is
   begin

      Success := False;

      if List.used_items = Max_Item then
         return;
      end if;

      for i in List.Items'Range loop

         pragma Loop_Invariant
           (for some j in i .. Max_Item => not List.Items (j).used);

         if not List.Items (i).used then
            List.Items (i).value := Value;
            List.Items (i).used  := True;
            List.used_items     := List.used_items + 1;
            Success := True;
            return;
         end if;
      end loop;

   end Append_Item;

end Array_Item_Lists;

Answer 3

Counting elements which have a given property in a data-structure is tricky to express indeed. To help with this problem, we provide with SPARK pro of generic counting function in the library of lemmas. This library of higher level functions is described in the user guide:

http://docs.adacore.com/spark2014-docs/html/ug/en/source/spark_libraries.html#higher-order-function-library

To use it, you should modify your project file to use the project file of the lemma library and set SPARK_BODY_MODE to Off.

You should also set the environment variable SPARK_LEMMAS_OBJECT_DIR to the absolute path of the object directory where you want compilation and verification artefacts for the lemma library to be created.

Then, you can instantiate SPARK.Higher_Order.Fold.Count for your purpose. It expects an unconstrained array type and a function to choose which elements should be counted. So I have rewritten your code to supply this information and instantiated the generic as follows:

   type t_item_list_b is array (positive range <>) of t_item;
   subtype t_item_list is t_item_list_b (1 .. MAX_ITEM);

   function Is_Used (X : t_item) return Boolean is
     (X.used);

   package Count_Used is new SPARK.Higher_Order.Fold.Count
     (Index_Type => Positive,
      Element    => t_item,
      Array_Type => t_item_list_b,
      Choose     => Is_Used);

Count_Used now contains:

• a Count function that you can use in your invariant:

  function invariant return boolean is
      (used_items = Count_Used.Count (items));
  

• lemmas to prove usual things for counting: Count_Zero to prove that the result of count is 0 is no elements have the property in the array, and Update_Count to know how Count is modified when the array is updated. These properties are obvious for a person, but in fact they need induction to prove, so they are generally out of reach of automatic solvers. To prove append_item, I now simply need to call Update_Count after the update of item as follows:

  procedure append_item
   (value    : in  integer;
    success  : out boolean)
   with ...
  is
    Old_Items : t_item_list := items with Ghost;
  begin
  
    if used_items = MAX_ITEM then
       success := false;
       return;
    end if;
  
    for i in items'range loop
       if not items(i).used then
          items(i).value := value;
          items(i).used  := true;
          used_items     := used_items + 1;
          success := true;
          Count_Used.Update_Count (items, Old_Items, I);
          return;
       end if;
    end loop;
  
    -- Should be unreachable
    raise program_error;
  end append_item;
  

I hope this helps,

Best Regards,

Answer 4

Using this spec for Append_Item doesn’t prove that Used_Items is equal to the number of used elements in the list, but (with the removal of the raise Program_Error) it does at least prove.

procedure Append_Item (Value : in  Integer; Success : out Boolean)
with Pre =>
  Used_Items <= Max_Item  -- avoid overflow check
  and
  (Used_Items = Max_Item
   or (for some Item of Items => not Item.Used)),
  Post =>
    (Used_Items'Old < Max_Item
     and Used_Items = Used_Items'Old + 1
     and Success = True)
    or (Used_Items'Old = Max_Item and Success = False);