Завершение цикла

Question

Я хочу доказать, что цикл в этой процедуре завершится, используя вариант (связанную функцию)

вариант будет I, а нижняя граница будет 0 (I: = 0)
при каждом повторении размер I будет уменьшаться, пока не достигнет нижней границы 0 Как я могу доказать, что I будет уменьшаться в этом цикле?

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

Если я напишу это в типичной ида идиоме, я получу

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;

Это короче и понятнее. Я не знаю, проще ли это доказать с помощью SPARK.

Answer 2

Я бы использовал конструкцию с ограниченным циклом (для цикла) для итерации по массиву.Цикл for легче обрабатывает границы массивов и пустые массивы.Это работает для меня в GNAT CE 2018 (здесь используется SPARK 2014):

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;

и

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 3

Я не уверен, что вы подразумеваете под «вариантом» и «связанной функцией», и у меня нет доступа к вашей версии SPARK.

В SPARK 2014, с GNAT CE 2018, это доказывает (после большой боли, может быть, мне стоит пройтись по некоторым учебникам SPARK) без каких-либо инвариантов цикла.

Я думаю, что я мог бы обойтись без Supported_Range, если бы запустил цикл в обратном порядке.

Мне бы хотелось заменить True в постусловии на (for all D of Data => D /= Key), но я оставлю это на этом.

Я понимаю, что это не отвечает на ваш вопрос, извините.

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;