GNATprove：简单函数中的“后置条件可能会失败”

Question

我想写一个简单的函数，找到给定的Integer数组中的最大数字。这是规格：

package Maximum with SPARK_Mode is

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

   function Maximum (A : in Vector) return Integer
     with
       SPARK_Mode,
       Pre => A'Length > 0,
         Post =>
         (for all i in A'Range => A(i) <= Maximum'Result)
         and then
           (for some i in A'Range => A(i) = Maximum'Result);

end Maximum;

这是功能的主体：

package body Maximum with SPARK_Mode is

   function Maximum (A : in Vector) return Integer
   is
   Max : Integer := A (A'First);
   begin
      if (A'Length = 1) then
         return Max;
      end if;

      for I in A'First + 1 .. A'Last loop
         pragma Loop_Invariant
           (for all Index in A'First .. I - 1 => Max >= A(Index));

         if A (I) > Max then
            Max := A (I);
         end if;
      end loop;

      return Max;
   end Maximum;

end Maximum;

当我试图用SPARK证明这个功能时，它说后置条件可能会失败。我现在正试着理解这个问题5个小时，我不知道为什么会这么说。这真的很烦人，这个功能必须起作用。你知道为什么SPARK表现得那么奇怪吗？这个函数的数据示例是什么，不能满足其后置条件？它总是返回一个直接取自给定数组的值，它总是最大的。

Answer 1

你的错误是使循环不变，这比后置条件弱：

规格：

package Maximum
  with SPARK_Mode
is

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

   function Maximum (A : in Vector) return Integer
     with
       Pre  => A'Length > 0,
       Post => (for all i in A'Range => A(i) <= Maximum'Result)
               and
               (for some i in A'Range => A(i) = Maximum'Result);

end Maximum;

执行：

package body Maximum with SPARK_Mode is

   function Maximum (A : in Vector) return Integer
   is
   Max : Integer := A (A'First);
   begin
      if (A'Length = 1) then
         return Max;
      end if;

      for K in A'First + 1 .. A'Last loop
         pragma Loop_Invariant
           ((for all  I in A'First .. K - 1 => A (I) <= Max)
            and
            (for some I in A'First .. K - 1 => A (I) = Max));

         if A (K) > Max then
            Max := A (K);
         end if;
      end loop;

      return Max;
   end Maximum;

end Maximum;

项目文件：

project Maximum is
   for Main use ("maximum");
end Maximum;