这是一个古老而有趣的问题。这里有一个迟来的答案,只是为了完整性和未来的参考。
博客帖子中给出了解决此类问题的主要“诀窍”
Taking on a Challenge in SPARK
张贴在AdaCore的网站上。
与一些答案已经提出的相反,您不能使用递归函数来证明求和。相反,你需要一个
ghost function
下面的例子可以用GNAT CE 2019证明,证明级别为1。
后处理条件略有改善
Sum_Acc
。另请参见
this
另一个例子的相关答案。
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;
