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

Question

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

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;