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

问题描述

我正在尝试在 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;

解决方法

Vector 是如何定义的？是不是类似

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

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

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