数组总数的 Spark-Ada 后置条件 [英] Spark-Ada postcondition for array total
问题描述
如何为对数组元素求和的函数编写 Spark 后置条件?(Spark 2014，但如果有人向我展示如何为早期的 Spark 做这件事，我应该能够适应它.)
How does one write a Spark postcondition for a function that sums the elements of an array? (Spark 2014, but if someone shows me how to do it for an earlier Spark I should be able to adapt it.)
如果我有:
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
在我的特定情况下，我不需要担心溢出(我知道初始化时的总数是多少，它只能单调减少).
I don't need to worry about overflow in my particular case (I know what the total was at initialisation, and it can only monotonically decrease).
大概我需要在实现中使用循环变体来帮助证明者，但这应该是后置条件的直接变体，所以我还不担心.
Presumably I'll need a loop variant in the implementation, to help the prover, but that should be straightforward variation of the postcondition, so I'm not worried about that yet.
推荐答案
这是一个古老但有趣的问题.这是一个迟到的答案，仅供完整性和未来参考.
This is an old, yet interesting question. Here's a late answer, just for completeness and future reference.
主要的技巧"关于如何解决这类问题的博客文章中给出了承担AdaCore 网站上发布的 SPARK 挑战.
The main "trick" on how to solve these kind of problems was given in the blog post Taking on a Challenge in SPARK posted on AdaCore's website.
与某些答案已经建议的相反，您不能使用递归函数来证明求和.相反，您需要一个 ghost 函数 如下例所示.该方法可以扩展以证明类似的列表折叠".操作，例如(条件)计数.
Opposed to what was already suggested by some of the answer's, you cannot use a recursive function to prove the summation. Instead, you need a ghost function as shown in the example below. The method can be extended in order to proof similar "list folding" operations such as (conditional) counting.
以下示例可以通过 GNAT CE 2019 证明，证明级别为 1.
The example below can be proven with GNAT CE 2019 with proof level 1.
2020 年 7 月更新
Sum_Acc 的后置条件的小改进.另请参阅此相关答案的另一个示例.
Small improvement in postcondition of Sum_Acc. See also this related answer for another example.
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;
这篇关于数组总数的 Spark-Ada 后置条件的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
