Menu
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?
348
In bubble sort algorithm, after each iteration of the loop largest element of the array is always placed at right most position. Therefore, the loop invariant condition is that at the end of i iteration right most i elements are sorted and in place. for (i = 0 to n-1) for (j = 0 to j arr[j+1]) swap(&arr[j], &arr[j+1]);
Termination: When the for-loop terminates j=(n−1)+1=n. Now the loop invariant gives: The variable answer contains the maximum of all numbers in subarray A[0:n]=A. This is exactly the value that the algorithm should output, and which it then outputs. Therefore the algorithm is correct.
A preserved invariant of a state machine M = (S, G ⊆ S × S, q0 ∈ S) is a predicate, P, on states, such that whenever P(q) is true of a state q, and q → r ∈ G, then P(r) is true.
For Algorithm 1, we’d prove the invariant in two steps. At the beginning of the loop, and . The sum is the sum of no numbers. We can use as its value, so we see that the invariant holds before the first iteration. Let’s say that the invariant holds at the beginning of the -th iteration:
How to Prove a Loop Invariant Proving an invariant is similar to mathematical induction. The requirement that the invariant hold before the first iteration corresponds to the base case of induction. The second condition is similar to the inductive step.
A weaker invariant that is also true is that i >= 0 && i <= 10. One may get confused between the loop invariant, and the loop conditional ( the condition which controls termination of the loop ). ( although it can temporarily be false during the body of the loop ).
Proving an invariant is similar to mathematical induction. The requirement that the invariant hold before the first iteration corresponds to the base case of induction. The second condition is similar to the inductive step. But, unlike induction that goes on infinitely, a loop invariant needs to hold only until the loop has ended.
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.
132
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
