8

我的目标是证明霍纳法则是正确的。为此，我将霍纳当前计算的值与“实数”多项式的值进行比较。
所以我做了这段代码：

package body Poly with SPARK_Mode is
   function Horner (X : Integer; A : Vector) return Integer is
      Y : Integer := 0;
      Z : Integer := 0 with Ghost;
   begin
      for I in reverse A'First .. A'Last loop
         pragma Loop_Invariant (Y * (X ** (I - A'First + 1)) = Z);
         Y := A(I) + Y * X;
         Z := Z + A(I) * (X ** (I - A'First));
      end loop;
      pragma Assert (Y = Z);
      return Y;
   end Horner;
end Poly;

这应该证明不变量。不幸的是， gnatprove 告诉我：

cannot prove  Y * (X ** (I - A'First + 1)) = Z
e.g. when A = (1 => 0, others => 0) and A'First = 0 and A'Last = 1 and I = 0 and X = 1 and Y = -1 and Z = 0

在这种情况下 Y=-1 是如何工作的？你有任何想法如何解决这个问题吗？

4

1 回答 1

11

这里的反例是虚假的，它不对应于真正的无效执行。该算术对于证明者来说太复杂了，这导致循环不变性保存未被证明，以及虚假的反例。

要调查这种未经证明的检查，您必须进入证明性质的“自动激活”模式，这需要将性质分解成较小的部分，直到自动证明者可以处理较小的步骤，或者您可以隔离未经证明的基本性质您可以在引理中隔离，您可以单独验证。

这里我在一个迭代开始时为 Y 的值引入了一个幽灵变量 YY，并在越来越小的断言中分解了循环不变量，这表明问题在于求幂 (X ** (I - A'First + 1) = X * (X ** (I - A'First)) 我也在一个断言中隔离：

package body Poly with SPARK_Mode is
   function Horner (X : Integer; A : Vector) return Integer is
      Y : Integer := 0;
      Z : Integer := 0 with Ghost;
      YY : Integer with Ghost;
   begin
      for I in reverse A'First .. A'Last loop
         pragma Loop_Invariant (Y * (X ** (I - A'First + 1)) = Z);
         YY := Y;
         Y := A(I) + Y * X;
         Z := Z + A(I) * (X ** (I - A'First));
         pragma Assert (Z = YY * (X ** (I - A'First + 1)) + A(I) * (X ** (I - A'First)));
         pragma Assert (X ** (I - A'First + 1) = X * (X ** (I - A'First)));
         pragma Assert (Z = YY * X * (X ** (I - A'First)) + A(I) * (X ** (I - A'First)));
         pragma Assert (Z = (YY * X + A(I)) * (X ** (I - A'First)));
         pragma Assert (Z = Y * (X ** (I - A'First)));
      end loop;
      pragma Assert (Y = Z);
      return Y;
   end Horner;
end Poly;

现在所有断言和循环不变量都使用 --level=2 和 SPARK 社区 2020 证明。当然有些断言是不需要的，因此您可以删除它们。

于 2021-03-24T20:29:53.550 回答