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

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 2

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);

Answer 3

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;