我的目标是证明霍纳法则是正确的。为此,我将 Horner 当前计算的值与“实数”多项式的值进行比较。
所以我做了这段代码:
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 是如何工作的?您对如何解决此问题有任何想法吗?