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

这是一个古老但有趣的问题。这是一个迟来的答案，仅供完整性和将来参考。

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

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

下面的示例可以使用 GNAT CE 2019 进行证明级别 1 的证明。

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;

Answer 2

编写后置条件的一种方法可以是递归函数。这样就可以避免实现和规范完全相同的问题。