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

问题描述

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

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

似乎（例如，在尝试手动校对时）函数InficientEuler1Sum2不了解InficientEuler1Sum的结构。向其提供此信息的最佳方法是什么？

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

解决方法

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

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

似乎很难。这种断言要求在两个函数上都具有后置条件，以使证明者确信该条件成立。我目前不知道该怎么做（其他人可能知道）。

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

因此，另一种（尽管不太令人兴奋的方法）是通过将两个方法置于同一个循环中，然后断言每种方法的累加等效性（{{1 }}）变量在循环中不变，并最终声明（如下所示）。其中一个变量被标记为"ghost" variable，因为实际上两次计算总和毫无意义：您仅需要第二个Sum变量用于证明。

对于以下示例：包装规格。和另一个SO answer中的主文件。

testing.adb

Sum

输出

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;