如何为对数组元素求和的函数编写 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
在我的特定情况下，我不需要担心溢出（我知道初始化时的总数是多少，它只能单调减少）。
大概我在实现中需要一个循环变体来帮助证明者，但这应该是后置条件的直接变体，所以我还不担心。
这是一个古老但有趣的问题。这是一个较晚的答案，仅供参考。
关于如何解决这类问题的主要“技巧”在AdaCore 网站上发布的博客文章Take on a Challenge in SPARK中给出。
与某些答案已经提出的相反，您不能使用递归函数来证明总和。相反，您需要一个ghost 函数，如下例所示。可以扩展该方法以证明类似的“列表折叠”操作，例如（条件）计数。
下面的示例可以通过 GNAT CE 2019 以证明级别 1 进行证明。
2020 年 7 月更新
后置条件的小改进Sum_Acc。另请参阅此相关答案以获取另一个示例。
总和广告
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;
总和.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;
编写后置条件的一种方法可以是递归函数。这将避免实现和规范完全相同的问题。