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

Question

我有两个函数:InefficientEuler1Sum 和 InefficientEuler1Sum2。我想证明它们是等价的(给定相同的输入相同的输出)。当我运行 SPARK -> Prove File(在 GNAT Studio 中)时，我在文件 euler1.adb 中收到关于 pragma Loop_Invariant(Sum = InefficientEuler1Sum(I)); 行的消息:

1. 循环不变式可能在第一次迭代中失败
2. 循环不变量可能不会被任意迭代保留

似乎(例如，在尝试手动证明时)函数 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));

似乎有点难。这样的断言需要两个函数的后置条件，这将使证明者相信这样的条件成立。我现在不知道该怎么做(尽管其他人可能知道)。

旁注:我在这里看到的主要困难是如何制定一个后置条件(在任一函数上)，它既描述了函数的输入和输出之间的关系，又，同时，可以使用合适的循环不变量来证明。制定这些合适的循环不变量似乎具有挑战性，因为 Sum 变量的更新模式在多次迭代中是周期性的(对于 InefficientEuler1Sum，周期为 5，对于 InefficientEuler1Sum2 是 15)。我不确定(此时)如何制定可以处理此类行为的循环不变量。

因此，另一种(虽然不那么令人兴奋的方法)是通过将它们放在一个公共(public)循环中然后断言每个方法的累加( Sum) 变量在循环不变和最终断言中(如下所示)。其中一个变量被标记为 "ghost" variable因为实际计算总和两次毫无意义:您需要第二个 Sum 变量仅用于证明。

对于以下示例:包规范。和另一个主文件 SO answer .

测试.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