在下面的例子中（并且反对其他答案 https://stackoverflow.com/a/57171268），我将计算部分和的 Ghost 函数分离到一个通用的 Ghost 包中SPARK_Fold。从这个包中我使用了 Ghost 函数Sum_Acc证明求和循环Calc_ST。套餐Example可以使用 GNAT CE 2020 进行证明，证明级别设置为 1。
基础方法的学分：AdaCore 博客文章 https://blog.adacore.com/taking-on-a-challenge-in-spark.
示例.ads
with SPARK_Fold;
package Example with SPARK_Mode is
subtype EEG_Reading_Index is Integer range 0 .. Integer'Last - 1;
subtype EEG_Reading is Integer range 0 .. 1;
type EEG_Readings is array (EEG_Reading_Index range <>) of EEG_Reading;
package Sum_EEG_Readings is
new SPARK_Fold.Sum
(Index_Type => EEG_Reading_Index,
Element_In => EEG_Reading,
List_Type => EEG_Readings,
Element_Out => Natural);
function Calc_ST (EEG : EEG_Readings) return Natural with
Pre => EEG'Length > 0,
Post => Calc_ST'Result = Sum_EEG_Readings.Sum_Acc (EEG) (EEG'Last);
end Example;
示例.adb（这里只是照常计算总和）。
package body Example with SPARK_Mode is
-------------
-- Calc_ST --
-------------
function Calc_ST (EEG : EEG_Readings) return Natural is
Result : Natural := EEG (EEG'First);
begin
for I in EEG'First + 1 .. EEG'Last loop
pragma Loop_Invariant
(Result = Sum_EEG_Readings.Sum_Acc (EEG) (I - 1));
Result := Result + EEG (I);
end loop;
return Result;
end Calc_ST;
end Example;
火花折叠.广告（通用帮助包）
package SPARK_Fold with Ghost is
-- Based on the blog post:
-- https://blog.adacore.com/taking-on-a-challenge-in-spark
---------
-- Sum --
---------
generic
type Index_Type is range <>;
type Element_In is range <>;
type List_Type is array (Index_Type range <>) of Element_In;
type Element_Out is range <>;
package Sum with Ghost is
type Partial_Sums is array (Index_Type range <>) of Element_Out;
function Sum_Acc (L : List_Type) 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 =>
abs (Sum_Acc'Result (I)) <= Element_Out (I - L'First + 1) * Element_Out (Element_In'Last))
and then (Sum_Acc'Result (L'First) = Element_Out (L (L'First)))
and then (for all I in L'First + 1 .. L'Last =>
Sum_Acc'Result (I) = Sum_Acc'Result (I - 1) + Element_Out (L (I)));
end Sum;
-----------
-- Count --
-----------
generic
type Index_Type is range <>;
type Element is range <>;
type List_Type is array (Index_Type range <>) of Element;
with function Choose (X : Element) return Boolean;
-- Count the number of elements for which Choose returns True.
package Count with Ghost is
type Partial_Counts is array (Index_Type range <>) of Natural;
function Count_Acc (L : List_Type) return Partial_Counts with
Ghost,
Pre => (L'Length > 0),
Post => (Count_Acc'Result'Length = L'Length)
and then (Count_Acc'Result'First = L'First)
and then (for all I in L'First .. L'Last =>
Count_Acc'Result (I) <= Natural (I) - Natural (L'First) + 1)
and then (Count_Acc'Result (L'First) = (if Choose (L (L'First)) then 1 else 0))
and then (for all I in L'First + 1 .. L'Last =>
Count_Acc'Result (I) = Count_Acc'Result (I - 1) + (if Choose (L (I)) then 1 else 0));
end Count;
end SPARK_Fold;
Spark_fold.adb
package body SPARK_Fold is
---------
-- Sum --
---------
package body Sum is
function Sum_Acc (L : List_Type) return Partial_Sums is
Result : Partial_Sums (L'Range) := (others => 0);
begin
Result (L'First) := Element_Out (L (L'First));
for Index in L'First + 1 .. L'Last loop
-- Head equal.
pragma Loop_Invariant
(Result (L'First) = Element_Out (L (L'First)));
-- Tail equal.
pragma Loop_Invariant
(for all I in L'First + 1 .. Index - 1 =>
Result (I) = Result (I - 1) + Element_Out (L (I)));
-- Result within bounds.
pragma Loop_Invariant
(for all I in L'First .. Index - 1 =>
abs (Result (I)) <= Element_Out (I - L'First + 1) * Element_Out (Element_In'Last));
Result (Index) := Result (Index - 1) + Element_Out (L (Index));
end loop;
return Result;
end Sum_Acc;
end Sum;
-----------
-- Count --
-----------
package body Count is
function Count_Acc (L : List_Type) return Partial_Counts is
Result : Partial_Counts (L'Range) := (others => 0);
begin
if Choose (L (L'First)) then
Result (L'First) := 1;
else
Result (L'First) := 0;
end if;
for Index in L'First + 1 .. L'Last loop
-- Head equal.
pragma Loop_Invariant
(Result (L'First) = (if Choose (L (L'First)) then 1 else 0));
-- Tail equal.
pragma Loop_Invariant
(for all I in L'First + 1 .. Index - 1 =>
Result (I) = Result (I - 1) + (if Choose (L (I)) then 1 else 0));
-- Bounds.
pragma Loop_Invariant
(for all I in L'First .. Index - 1 =>
Result (I) <= Natural (I) - Natural (L'First) + 1);
if Choose (L (Index)) then
Result (Index) := Result (Index - 1) + 1;
else
Result (Index) := Result (Index - 1) + 0;
end if;
end loop;
return Result;
end Count_Acc;
end Count;
end SPARK_Fold;
