I have two functions: InefficientEuler1Sum and InefficientEuler1Sum2. I want to prove that they both are equivalent (same output given same input).
When I run SPARK -> Prove File (in GNAT Studio), I get such messages about line pragma Loop_Invariant(Sum = InefficientEuler1Sum(I)); in the file euler1.adb:
loop invariant might fail in first iterationloop invariant might not be preserved by an arbitrary iterationIt seems (for example, when trying manual proof) that function InefficientEuler1Sum2 has no idea about structure of InefficientEuler1Sum. What's the best way to give this information to it?
File euler1.ads:
package Euler1 with
SPARK_Mode
is
function InefficientEuler1Sum (N: Natural) return Natural with
Ghost,
Pre => (N <= 1000);
function InefficientEuler1Sum2 (N: Natural) return Natural with
Ghost,
Pre => (N <= 1000),
Post => (InefficientEuler1Sum2'Result = InefficientEuler1Sum (N));
end Euler1;
File euler1.adb:
package body Euler1 with
SPARK_Mode
is
function InefficientEuler1Sum(N: Natural) return Natural is
Sum: Natural := 0;
begin
for I in 0..N loop
if I mod 3 = 0 or I mod 5 = 0 then
Sum := Sum + I;
end if;
pragma Loop_Invariant(Sum <= I * (I + 1) / 2);
end loop;
return Sum;
end InefficientEuler1Sum;
function InefficientEuler1Sum2 (N: Natural) return Natural is
Sum: Natural := 0;
begin
for I in 0..N loop
if I mod 3 = 0 then
Sum := Sum + I;
end if;
if I mod 5 = 0 then
Sum := Sum + I;
end if;
if I mod 15 = 0 then
Sum := Sum - I;
end if;
pragma Loop_Invariant(Sum <= 2 * I * I);
pragma Loop_Invariant(Sum = InefficientEuler1Sum(I));
end loop;
return Sum;
end InefficientEuler1Sum2;
end Euler1;
Proving that the two functions are equivalent using an assertion like:
pragma Assert
(for all I in 0 .. 1000 =>
Inefficient_Euler_1_Sum (I) = Inefficient_Euler_1_Sum_2 (I));
seems kind of hard. Such an assertion requires post-conditions on both functions that would convince the prover that such a condition holds. I don't know how to do this at this point (others may know though).
Side-note: The main difficulty I see here is how to formulate a post-condition (on either function) that both describes the relation between the function's input and the output, and, at the same time, can be proven using suitable loop invariants. Formulating these suitable loop invariants seems challenging as the update pattern of the Sum variable is periodic over multiple iterations (for InefficientEuler1Sum the period is 5, for InefficientEuler1Sum2 it's 15). I'm not sure (at this point) how to formulate a loop invariant that can deal with this kind of behavior.
Hence, another (though less exciting approach) would be to show the equivalence of both methods by putting them in a common loop and then asserting the equivalence of each of the method's accumulation (Sum) variable in a loop invariant and final assertion (as shown below). One of the variables is marked as a "ghost" variable as it's pointless to actually compute the sum twice: you need a second Sum variable only for the proof.
For the example below: package spec. and a main file as in the other SO answer.
testing.adb
package body Testing with SPARK_Mode is
-------------------------------
-- Inefficient_Euler_1_Sum_2 --
-------------------------------
function Inefficient_Euler_1_Sum_2 (N : Domain) return Natural is
Sum_1 : Natural := 0;
Sum_2 : Natural := 0 with Ghost;
begin
for I in 0 .. N loop
-- Method 1
begin
if I mod 3 = 0 then
Sum_1 := Sum_1 + I;
end if;
if I mod 5 = 0 then
Sum_1 := Sum_1 + I;
end if;
if I mod 15 = 0 then
Sum_1 := Sum_1 - I;
end if;
end;
-- Method2
begin
if I mod 3 = 0 or I mod 5 = 0 then
Sum_2 := Sum_2 + I;
end if;
end;
pragma Loop_Invariant (Sum_1 <= (2 * I) * I);
pragma Loop_Invariant (Sum_2 <= I * (I + 1) / 2);
pragma Loop_Invariant (Sum_1 = Sum_2);
end loop;
pragma Assert (Sum_1 = Sum_2);
return Sum_1;
end Inefficient_Euler_1_Sum_2;
end Testing;
output
$ gnatprove -Pdefault.gpr -j0 --level=1 --report=all
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
main.adb:5:19: info: assertion proved
testing.adb:18:18: info: division check proved
testing.adb:19:31: info: overflow check proved
testing.adb:21:18: info: division check proved
testing.adb:22:31: info: overflow check proved
testing.adb:24:18: info: division check proved
testing.adb:25:31: info: overflow check proved
testing.adb:25:31: info: range check proved
testing.adb:31:18: info: division check proved
testing.adb:31:33: info: division check proved
testing.adb:32:31: info: overflow check proved
testing.adb:36:33: info: loop invariant initialization proved
testing.adb:36:33: info: loop invariant preservation proved
testing.adb:36:45: info: overflow check proved
testing.adb:36:50: info: overflow check proved
testing.adb:37:33: info: loop invariant initialization proved
testing.adb:37:33: info: loop invariant preservation proved
testing.adb:37:44: info: overflow check proved
testing.adb:37:49: info: overflow check proved
testing.adb:37:54: info: division check proved
testing.adb:38:33: info: loop invariant initialization proved
testing.adb:38:33: info: loop invariant preservation proved
testing.adb:42:22: info: assertion proved
testing.ads:18:19: info: postcondition proved
Summary logged in /obj/gnatprove/gnatprove.out