GNATprove："postcondition might fail" 简单函数

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 的行为如此奇怪吗？此函数未满足其后置条件的数据示例是什么？它总是 returns 直接从给定数组中获取的值，并且它始终是最大值。

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;

GNATprove："postcondition might fail" 简单函数

GNATprove: "postcondition might fail" in simple function

formal-verification

ada

gnat

spark-ada

spark-2014