如何证明这个不变量? [英] How to prove this invariant?

问题描述

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

带有 SPARK_Mode 的包体 Poly 是函数 Horner (X : Integer; A : Vector) return Integer isY : 整数 := 0;Z : 整数 := 0 与 Ghost;开始对于我在反向 A'First .. A'Last 循环pragma Loop_Invariant (Y * (X ** (I - A'First + 1)) = Z);Y := A(I) + Y * X;Z := Z + A(I) * (X ** (I - A'First));结束循环；pragma Assert (Y = Z);返回 Y;结束霍纳；端聚；

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

不能证明 Y * (X ** (I - A'First + 1)) = Z例如当 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 是如何工作的?您对如何解决此问题有任何想法吗?

解决方案

这里的反例是虚假的，它不对应于真正的无效执行.算法过于复杂，证明者无法得到，导致循环不变性不成立，反例不成立.

要调查这种未经证实的检查，您必须输入自动激活"证明属性的模式，这需要将属性分解为更小的属性，直到自动证明器可以处理更小的步骤，或者您可以隔离未证明的基本属性，您可以将其隔离在引理中，您可以单独验证.

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

带有 SPARK_Mode 的包体 Poly 是函数 Horner (X : Integer; A : Vector) return Integer isY : 整数 := 0;Z : 整数 := 0 与 Ghost;YY : 带有 Ghost 的整数；开始对于我在反向 A'First .. A'Last 循环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)));结束循环；pragma Assert (Y = Z);返回 Y;结束霍纳；端聚；

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

I aim to prove that the Horner's Rule is correct. To do so, I compare the value currently calculated by Horner with the value of "real" polynominal.
So I made this piece of code:

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;

Which should prove the invariant. Unfortunately, gnatprove tells me:

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

How does it work that Y=-1 in this case? Do you have any ideas how to fix this?

解决方案

the counterexample here is spurious, it does not correspond to a real invalid execution. The arithmetic is too complex for provers to get, which leads both to the loop invariant preservation not being proved, and the spurious counterexample.

To investigate such an unproved check, you must enter the "auto-active" mode of proving properties, which requires to break down the property in smaller ones until either automatic provers can deal with the smaller steps, or you can isolate an unproved elementary property that you can isolate in a lemma, that you can verify separately.

Here I introduced a ghost variable YY for the value of Y at the beginning of an iteration, and broke down the loop invariant in smaller and smaller assertions, which showed that the problem was the exponentiation (X ** (I - A'First + 1) = X * (X ** (I - A'First)) that I also isolated in an assertion:

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;

Now all assertions and the loop invariant are proved using --level=2 with SPARK Community 2020. Of course some assertions are not needed, so you can remove them.

这篇关于如何证明这个不变量?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！