ada - 数组总数的 Spark-Ada 后置条件

Question

如何为对数组元素求和的函数编写 Spark 后置条件？ (Spark 2014，但如果有人告诉我如何为更早的 Spark 做这件事，我应该能够适应它。)

如果我有:

type Positive_Array is array (Positive range <>) of Positive;

function Array_Total(The_Array: Positive_Array) return Positive
with
  Post => Array_Total'Return = -- What goes here?
is
  -- and so on

在我的特定情况下，我不需要担心溢出(我知道初始化时的总数，它只能单调减少)。

大概我在实现中需要一个循环变体，以帮助证明者，但这应该是后置条件的直接变体，所以我还不担心。

Answer 1

这是一个古老但有趣的问题。这是一个迟到的答案，只是为了完整性和 future 引用。

博文 Taking on a Challenge in SPARK 中给出了解决此类问题的主要“技巧”发布在 AdaCore 的网站上。

与某些答案已经提出的相反，您不能使用递归函数来证明求和。相反，您需要一个 ghost function如下例所示。可以扩展该方法以证明类似的“列表折叠”操作，例如(条件)计数。

下面的例子可以用证明级别 1 的 GNAT CE 2019 证明。

2020 年 7 月更新

Sum_Acc 的后置条件略有改进。另见 this另一个例子的相关答案。

sum.ads

package Sum with SPARK_Mode is

   --  The ranges of the list's index and element discrete types must be
   --  limited in order to prevent overflow during summation, i.e.:
   --
   --     Nat'Last * Int'First >= Integer'First   and
   --     Nat'Last * Int'Last  <= Integer'Last
   --
   --  In this case +/-1000 * +/-1000 = +/-1_000_000 which is well within the 
   --  range of the Ada Integer type on typical platforms.
   
   subtype Int is Integer range -1000 .. 1000;
   subtype Nat is Integer range     0 .. 1000;
   
   type List is array (Nat range <>) of Int;
   
   
   --  The function "Sum_Acc" below is Ghost code to help the prover proof the
   --  postcondition (result) of the "Sum" function. It computes a list of
   --  partial sums. For example:
   --
   --     Input   :  [ 1  2  3  4  5  6 ]
   --     Output  :  [ 1  3  6 10 15 21 ]
   --
   --  Note that the lengths of lists are the same, the first elements are
   --  identical and the last element of the output (here: "21"), is the
   --  result of the actual function under consideration, "Sum".
   --
   --  REMARK: In this case, the input of "Sum_Acc" and "Sum" is limited
   --          to non-empty lists for convenience.
   
   type Partial_Sums is array (Nat range <>) of Integer;
   
   function Sum_Acc (L : List) return Partial_Sums with 
     Ghost,
     Pre  =>  (L'Length > 0),
     Post =>  (Sum_Acc'Result'Length = L'Length) 
     and then (Sum_Acc'Result'First = L'First) 
     and then (for all I in L'First .. L'Last =>
                 Sum_Acc'Result (I) in 
                   (I - L'First + 1) * Int'First .. 
                   (I - L'First + 1) * Int'Last)
     and then (Sum_Acc'Result (L'First) = L (L'First))
     and then (for all I in L'First + 1 .. L'Last =>
                 Sum_Acc'Result (I) = Sum_Acc'Result (I - 1) + L (I));
   
   
   function Sum (L : List) return Integer with
     Pre  => L'Length > 0,
     Post => Sum'Result = Sum_Acc (L) (L'Last);

end Sum;

sum.adb

package body Sum with SPARK_Mode is

   -------------
   -- Sum_Acc --
   -------------
            
   function Sum_Acc (L : List) return Partial_Sums is
      PS : Partial_Sums (L'Range) := (others => 0);
   begin
      
      PS (L'First) := L (L'First);
      
      for Index in L'First + 1 .. L'Last loop
      
         --  Head equal.
         pragma Loop_Invariant
           (PS (L'First) = L (L'First));
         
         --  Tail equal.
         pragma Loop_Invariant
           (for all I in L'First + 1 .. Index - 1 =>
              PS (I) = PS (I - 1) + L (I)); 
         
         --  NOTE: The loop invariant below holds only when the range of "Int" 
         --        is symmetric, i.e -Int'First = Int'Last. If not, then this
         --        loop invariant may have to be adjusted.
         
         --  Result within bounds.
         pragma Loop_Invariant 
           (for all I in L'First .. Index - 1 =>
              PS (I) in (I - L'First + 1) * Int'First ..
                        (I - L'First + 1) * Int'Last);
               
         PS (Index) := PS (Index - 1) + L (Index);
      
      end loop;
      
      return PS;
      
   end Sum_Acc;

   ---------
   -- Sum --
   ---------
   
   function Sum (L : List) return Integer is
      Result : Integer := L (L'First);
   begin
      
      for I in L'First + 1 .. L'Last loop
         
         pragma Loop_Invariant
           (Result = Sum_Acc (L) (I - 1));
         
         Result := Result + L (I);
        
      end loop;
      
      return Result;
      
   end Sum;

end Sum;