如何证明两个函数的等价性？

Question

我有两个函数：InefficientEuler1Sum 和 InefficientEuler1Sum2。我想证明它们是等价的（给定相同的输入相同的输出）。当我运行 SPARK -> Prove File（在 GNAT Studio 中）时，我在文件 euler1.adb:

中收到关于行 pragma Loop_Invariant(Sum = InefficientEuler1Sum(I)); 的消息

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

似乎（例如，在尝试手动证明时）函数 InefficientEuler1Sum2 不知道 InefficientEuler1Sum 的结构。向它提供此信息的最佳方式是什么？

文件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;

文件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;

Answer 1

使用如下断言证明这两个函数是等价的：

pragma Assert
  (for all I in 0 .. 1000 =>
     Inefficient_Euler_1_Sum (I) = Inefficient_Euler_1_Sum_2 (I));

好像有点难。这样的断言需要对两个函数都使用 post-conditions，这将使证明者相信这样的条件成立。我现在不知道该怎么做（虽然其他人可能知道）。

Side-note：我在这里看到的主要困难是如何制定一个post-condition（在任一函数上）都描述函数的输入和输出之间的关系，同时，可以使用合适的循环不变量来证明。制定这些合适的循环不变量似乎具有挑战性，因为 Sum 变量的更新模式在多次迭代中是周期性的（对于 InefficientEuler1Sum，周期为 5，对于 InefficientEuler1Sum2，周期为 15）。我不确定（此时）如何制定可以处理这种行为的循环不变量。

因此，另一种（尽管不那么令人兴奋的方法）是通过将这两种方法放在一个公共循环中然后断言每个方法的等价性来显示它们的等价性accumulation (Sum) variable in a loop invariant and final assertion（如下所示）。其中一个变量被标记为 "ghost" variable，因为实际计算两次总和是没有意义的：您需要第二个 Sum 变量仅用于证明。

对于以下示例：包规范。和另一个 .

中的主文件

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;

输出

$ 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

如何证明两个函数的等价性？

How to prove equivalence of two functions?

ada

spark-ada