I aim to prove that the Horner's Rule is correct. To do so, I compare the value currently calculated by Horner with the value of "real" polynominal.
So I made this piece of code:
package body Poly with SPARK_Mode is
function Horner (X : Integer; A : Vector) return Integer is
Y : Integer := 0;
Z : Integer := 0 with Ghost;
begin
for I in reverse A'First .. A'Last loop
pragma Loop_Invariant (Y * (X ** (I - A'First + 1)) = Z);
Y := A(I) + Y * X;
Z := Z + A(I) * (X ** (I - A'First));
end loop;
pragma Assert (Y = Z);
return Y;
end Horner;
end Poly;
Which should prove the invariant. Unfortunately, gnatprove tells me:
cannot prove Y * (X ** (I - A'First + 1)) = Z
e.g. when A = (1 => 0, others => 0) and A'First = 0 and A'Last = 1 and I = 0 and X = 1 and Y = -1 and Z = 0
How does it work that Y=-1 in this case? Do you have any ideas how to fix this?
X ** V
has an upper bound which includes showing the upper bound forX
andV = I - A'First + 1
separately. Although this might still be to hard for the prover.