CODEWITHSUNDEEP
adaspark-ada
Lessness Randomness
Lessness Randomness

Reputation: 158

How to prove equivalence of two functions?

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:

  1. loop invariant might fail in first iteration
  2. loop invariant might not be preserved by an arbitrary iteration

It 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;

Upvotes: 3

Views: 241

Answers (1)

DeeDee
DeeDee

Reputation: 5941

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

Upvotes: 4

Related Questions