Verifying loop termination

Question

I want to prove that the loop in this procedure will terminate using the variant ( bound function)

the variant will be I and the lower bound is 0 (I: = 0)
on each repetition, the size of I will decrease till reached to lower bound 0 How can I prove that I will decrease in this loop?

procedure Find
   (Key: Integer;
    Data : in MyArray;
    Index: out Integer;
    Found: out Boolean)
    --# post (Found -> Data(Index) = Key);
is
   I: Integer;
begin
   I := 0;
   Found := False;
   loop
      --# assert (I >= 0) and
      --# (I <= Data'Last + 1) and
      --# (Found -> Data(I) = Key);
      exit when (I > Data 'Last) or Found;
      if(Data(I)) = Key
      then
         Found := True;
      else
         I:= I + 1;
      end if;
   end loop;
   Index := I;
end Find;

Answer 1

I would use a bounded loop construct (for loop) to iterate over the array. A for loop handles array bounds and empty arrays more easily. This works for me in GNAT CE 2018 (using SPARK 2014 here):

package Foo with SPARK_Mode => On is

   type MyArray is array (Integer range <>) of Integer;

   procedure Find
     (Key   : in  Integer;
      Data  : in  MyArray;
      Index : out Integer;
      Found : out Boolean)
     with       
       Post => (if Found then Data (Index) = Key);

end Foo;

and

package body Foo with SPARK_Mode => On is

   ----------
   -- Find --
   ----------

   procedure Find
     (Key   : in  Integer;
      Data  : in  MyArray;
      Index : out Integer;
      Found : out Boolean)
   is
   begin

      Found := False;
      Index := Data'First;

      for I in Data'Range loop

         if Data (I) = Key then
            Found := True;   
            Index := I;
         end if;       

         pragma Loop_Invariant
           (Index in Data'Range);

         pragma Loop_Invariant
           (if Found then Data (Index) = Key else Data (Index) /= Key);        

         exit when Found;
      end loop;

   end Find;

end Foo;

Answer 2

If I write this in typical Ada idiom I get

package SPARK_Proof is
   type Integer_List is array (Positive range <>) of Integer;

   type Find_Result (Found : Boolean := False) is record
      case Found is
      when False =>
         null;
      when True =>
         Index : Positive;
      end case;
   end record;

   function Match_Index (Value : Integer; List : Integer_List) return Find_Result;
end SPARK_Proof;

package body SPARK_Proof is
   function Match_Index (Value : Integer; List : Integer_List) return Find_Result is
      -- Empty
   begin -- Match_Index
      Search : for I in List'Range loop
         if Value = List (I) then
            return (Found => True, Index => I);
         end if;
      end loop Search;

      return (Found => False);
   end Match_Index;
end SPARK_Proof;

This is shorter and clearer. I don't know if it's any easier to prove with SPARK.

Answer 3

I’m not sure what you mean by 'variant' and 'bound function', and I don’t have access to your version of SPARK.

In SPARK 2014, with GNAT CE 2018, this proves (after much pain, maybe I should work through some of the SPARK tutorials) without any loop invariants.

I think I could get away without Supported_Range if I ran the loop in reverse.

I’d’ve liked to replace the True in the postcondition with (for all D of Data => D /= Key), but I’ll leave it at that.

I realise this doesn’t answer your question, sorry.

package Memo with SPARK_Mode is
   subtype Supported_Range is Natural range 0 .. Natural'Last - 1;
   type My_Array is array (Supported_Range range <>) of Integer;
   procedure Find
     (Key   :     Integer;
      Data  :     My_Array;
      Index : out Integer;
      Found : out Boolean)
   with
     Pre => Data'Length >= 1,
     Post => ((Found and then Index in Data'Range and then Data (Index) = Key)
              or else True);
end Memo;

package body Memo with SPARK_Mode is
   procedure Find
     (Key   :     Integer;
      Data  :     My_Array;
      Index : out Integer;
      Found : out Boolean)
   is
      subtype Possible_J is Integer range Data’Range;
      J : Possible_J;
   begin
      J := Possible_J'First;
      Index := -1;  -- have to initialize with something
      Found := False;
      loop
         if Data (J) = Key
         then
            Found := True;
            Index := J;
            exit;
         else
            exit when J = Data'Last;
            J := J + 1;
         end if;
      end loop;
   end Find;
end Memo;