验证循环终止

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

我不确定您所说的“变体”和“绑定函数”是什么意思，而且我无法访问您的 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;

Answer 2

如果我用典型的 Ada 习语写这篇文章，我会得到

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 3

我会使用有界循环构造（for 循环）来遍历数组。 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;