小编s7e*_*g1a的帖子

我正在尝试在 Spark 中编写代码，使用 Horner 方法计算多项式的值。变量Result由Horner计算，变量Z以经典方式计算。我做了很多不同的测试，我的循环不变式总是正确的。但是，我收到消息：

loop invariant might not be preserved by an arbitrary iteration

是否存在循环不变量不起作用的情况，或者您是否需要向不变量添加更多条件？

这是我的主函数，它调用我的 Horner 函数：

  with Ada.Integer_Text_IO;
  use Ada.Integer_Text_IO;

  with Poly;
  use Poly;

  procedure Main is
     X : Integer;
     A : Vector (0 .. 2);
  begin
     X := 2;
     A := (5, 10, 15);

     Put(Horner(X, A));
  end Main;

和霍纳函数：

package body Poly with SPARK_Mode is
function Horner (X : Integer; A : Vector) 
  return Integer 
  is

  Result : Integer := 0;
  Z …