如何证明这个不变量？

Question

我旨在证明霍纳规则（Horner's Rule）的正确性。为此，我将当前由霍纳计算得到的值与“真实”多项式的值进行比较。
因此，我编写了以下代码：

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是如何工作的？您有任何修复的想法吗？

- qutrupali

---

我不会过于关注这里的反例。由于使用幂运算，它很可能无法证明。这对证明者来说是一个非常困难的操作。一个好的开始是分离底数和指数。例如，您必须证明 X ** V 有一个上界，其中包括单独显示 X 和 V = I - A'First + 1 的上界。尽管这可能仍然对证明者来说太难了。 - jklmnn

Answer 1

这里的反例是虚假的，它并不对应于真正的无效执行。算术太复杂了，使得证明者无法理解，这导致循环不变量未能得到证明，也导致了虚假的反例。

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

我在这里引入了一个名为YY的幽灵变量，用于记录迭代开始时Y的值，并将循环不变量分解成越来越小的断言，这表明问题出在指数运算（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;

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

- Yannick Moy