Why my loop invariant might not be preserved by any iteration?

Question

I'm trying to write a code in Spark that computes the value of the polynomial using the Horner method. The variable Result is calculated by Horner, and the variable Z is calculated in the classical way. I've done a lot of different tests and my loop invariant is always true. However, I get the message:

loop invariant might not be preserved by an arbitrary iteration

Are there any cases where the loop invariant doesn't work or do you need to add some more conditions to the invariant?

Here's my main func which call my Horner function:

  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;

And Horner function:

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;

A similar question has been answered [here](https://stackoverflow.com/a/66788892). — DeeDee, Jun 22 '21 at 07:53

score 5 · Accepted Answer · answered Jun 22 '21 at 13:27

How is Vector defined? Is it something like

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

In this case maybe the condition could fail if some indexes of A are negative. Also, does the invariant hold even if the first index of A is not zero? Maybe another case when the invariant fails is when A'Last = Integer'Last; in this case the i+1 would overflow.

Usually SPARK gives a reason, a counterexample, when it is not able to prove something. I would suggest you to check that, it can give you an idea of when the invariant fails. Keep in mind that the counterexamples are sometimes some very extreme case such as A'Last = Integer'Last. If this is the case you need to tell SPARK that A'Last = Integer'Last will never happen, maybe by defining a specific subtype for Vector index or by adding a contract to your function.

Why my loop invariant might not be preserved by any iteration?

1 Answers1