问题描述
我正在SPARK Ada中编写一个软件，该软件需要后置条件来验证函数返回值等于数组的求和值.在证明该函数所在的文件后，我不断收到一个错误，该错误不会完全累加，也没有双关语(我将发布代码的屏幕快照，以便更好地查看).大小为10的数组中唯一允许的值为0s或1s.
I am writing a piece of software in SPARK Ada which requires the post-condition to verify that the function return value is equal to the summed values of an array. Upon proving the file where the function resides, I keep getting an error which doesn't quite add up, no pun intended (I will post screenshots of the code so as to allow a better look). The only acceptable values allowed in the array of size 10 are 0s or 1s.
推荐答案
在下面的示例中(与其他答案相反 )，将将部分和计算出来的虚影函数分离到通用虚影包SPARK_Fold中.从这个包中，我使用重影函数Sum_Acc来证明Calc_ST中的求和循环.包Example可以使用GNAT CE 2020进行证明，证明级别设置为1.
In the example below (and opposed to the other answer), I separated the ghost function that computes the partial sum into a generic ghost package SPARK_Fold. From this package I use the ghost function Sum_Acc to proof the summation loop in Calc_ST. The package Example can be proven using GNAT CE 2020 with prove level set to 1.
该基础方法的积分: AdaCore博客文章.
example.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;
example.adb (此处仅照常计算总和).
example.adb (just computing the sum as usual here).
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;
spark_fold.ads (通用帮助程序包)
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;
这篇关于“应对SPARK Ada中的挑战"； -后置条件下的Ghost函数具有意外行为的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！