How to use Assert and loop_invariants

Question

Specification:

package PolyPack with SPARK_Mode is 
type Vector is array (Natural range <>) of Integer;
function RuleHorner (X: Integer; A : Vector) return Integer
with
Pre => A'Length > 0 and A'Last < Integer'Last;
end PolyPack ; 

I want to write body of PolyPack package with Assert and loop_invariants that the gnatprove program can prove my function RuleHorner correctness.

I write my function Horner but I don;t know how put assertions and loop_invariants in this program to prove its corectness :

with Ada.Integer_Text_IO;
package body PolyPack with SPARK_Mode is

   function RuleHorner (X: Integer; A : Vector) return Integer is
      Y : Integer := 0;
      begin       
      for I in 0 .. A'Length - 1 loop
         Y := (Y*X) + A(A'Last - I);
      end loop;
      return Y;
      end RuleHorner ;
end PolyPack ;

gnatprove :

overflow check might fail (e.g. when X = 2 and Y = -2)
overflow check might fail

overflow check are for line Y := (Y*X) + A(A'Last - I);

Can someone help me how remove overflow check with loop_invariants

Answer 1

The analysis is correct. The element type for type Vector is Integer. When X = 2, Y = -2, and A(A'Last - I) is less than Integer'First + 4 an underflow will occur. How do you think this should be handled in your program? Loop invariants will not work here because you cannot prove that an overflow or underflow cannot occur. Is there a way you can design your types and/or subtypes used within Vector and for variables X and Y to prevent Y from overflowing or underflowing?

I am also curious why you want to ignore the last value in your Vector. Are you trying to walk through the array in reverse? If so simply use the following for loop syntax:

for I in reverse A'Range loop