如何证明这个不变量？

问题描述

我的目标是证明霍纳法则是正确的。为此，我将 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 是如何工作的？您对如何解决此问题有任何想法吗？

解决方法

暂无找到可以解决该程序问题的有效方法，小编努力寻找整理中！

如果你已经找到好的解决方法，欢迎将解决方案带上本链接一起发送给小编。

小编邮箱:dio#foxmail.com (将#修改为@）