8

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?

1
  • i wouldn't concentrate too much on the counterexample here. It is likely that it doesn't prove due to using the power here. This is a really hard operation for the prover. A good start would be to separate the base and the exponent. E.g. you have to prove that X ** V has an upper bound which includes showing the upper bound for X and V = I - A'First + 1 separately. Although this might still be to hard for the prover.
    – jklmnn
    Commented Mar 24, 2021 at 20:21

1 Answer 1

11

the counterexample here is spurious, it does not correspond to a real invalid execution. The arithmetic is too complex for provers to get, which leads both to the loop invariant preservation not being proved, and the spurious counterexample.

To investigate such an unproved check, you must enter the "auto-active" mode of proving properties, which requires to break down the property in smaller ones until either automatic provers can deal with the smaller steps, or you can isolate an unproved elementary property that you can isolate in a lemma, that you can verify separately.

Here I introduced a ghost variable YY for the value of Y at the beginning of an iteration, and broke down the loop invariant in smaller and smaller assertions, which showed that the problem was the exponentiation (X ** (I - A'First + 1) = X * (X ** (I - A'First)) that I also isolated in an assertion:

package body Poly with SPARK_Mode is
   function Horner (X : Integer; A : Vector) return Integer is
      Y : Integer := 0;
      Z : Integer := 0 with Ghost;
      YY : Integer with Ghost;
   begin
      for I in reverse A'First .. A'Last loop
         pragma Loop_Invariant (Y * (X ** (I - A'First + 1)) = Z);
         YY := Y;
         Y := A(I) + Y * X;
         Z := Z + A(I) * (X ** (I - A'First));
         pragma Assert (Z = YY * (X ** (I - A'First + 1)) + A(I) * (X ** (I - A'First)));
         pragma Assert (X ** (I - A'First + 1) = X * (X ** (I - A'First)));
         pragma Assert (Z = YY * X * (X ** (I - A'First)) + A(I) * (X ** (I - A'First)));
         pragma Assert (Z = (YY * X + A(I)) * (X ** (I - A'First)));
         pragma Assert (Z = Y * (X ** (I - A'First)));
      end loop;
      pragma Assert (Y = Z);
      return Y;
   end Horner;
end Poly;

Now all assertions and the loop invariant are proved using --level=2 with SPARK Community 2020. Of course some assertions are not needed, so you can remove them.

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.