为什么我的循环不变量可能不会被任何迭代保留？

Question

我正在尝试在 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 : Integer := 0;

  begin
     for i in reverse A'Range loop
        
        pragma Loop_Invariant (Z=Result*(X**(i+1)));

        Result := Result*X + A(i); 
        Z := Z + A(i)*X**(i);

     end loop;

     pragma Assert (Result = Z);

     return Result;
end Horner;
end Poly;

Answer 1

是如何Vector定义的？是不是有点像

type Vector is array(Integer range <>) of Float;

在这种情况下，如果某些索引为A负，则条件可能会失败。此外，即使 的第一个索引A不为零，不变量是否成立？也许不变量失败的另一种情况是 when A'Last = Integer'Last; 在这种情况下，i+1将溢出。

通常 SPARK 会给出一个理由，一个反例，当它不能证明某事时。我建议您检查一下，它可以让您了解不变量何时失败。请记住，反例有时是一些非常极端的情况，例如A'Last = Integer'Last. 如果是这种情况，您需要告诉 SPARK 这A'Last = Integer'Last将永远不会发生，可能是通过为Vector索引定义特定的子类型或向您的函数添加合同。