无法证明阿达·斯帕克看似微不足道的平等

Question

所以我有这两个文件。

测试.ads

package Testing with
SPARK_Mode
is
function InefficientEuler1Sum2 (N: Natural) return Natural;
procedure LemmaForTesting with
Ghost,
Post => (InefficientEuler1Sum2(0) = 0);
end Testing;

和测试.adb

package body Testing with
SPARK_Mode
is
function InefficientEuler1Sum2 (N: Natural) return Natural is
Sum: Natural := 0;
begin
for I in 0..N loop
if I mod 3 = 0 then
Sum := Sum + I;
end if;
if I mod 5 = 0 then
Sum := Sum + I;
end if;
if I mod 15 = 0 then
Sum := Sum - I;
end if;
end loop;
return Sum;
end InefficientEuler1Sum2;
procedure LemmaForTesting
is
begin
null;
end LemmaForTesting;
end Testing;

当我运行SPARK->证明文件，我得到这样的信息：

GNATprove
E:AdaTesting SPARKsearchsrctesting.ads
10:14 medium: postcondition might fail
cannot prove InefficientEuler1Sum2(0) = 0

为什么会这样？我误解了什么或做错了什么？提前谢谢。

Answer 1

要证明平凡的等式，需要确保它被函数的后置条件覆盖。如果是这样，您可以使用一个简单的Assert语句来证明等式，如下例所示。在这一点上不需要引理。

然而，后置条件不足以证明不存在运行时错误(AoRTE(：给定函数的允许输入范围，对于N的某些值，求和可能会溢出。为了缓解这个问题，您需要绑定N的输入值，并使用循环不变量向证明者显示Sum的值在循环期间保持有界(有关循环不变量的一些背景信息，请参阅此处、此处和此处(。为了便于说明，我选择了(2 * I) * I的保守界，这将严重限制输入值的允许范围，但确实允许证明者证明在示例中没有运行时错误。

测试.ads

package Testing with SPARK_Mode is
--  Using the loop variant in the function body, one can guarantee that no
--  overflow will occur for all values of N in the range 
--
--     0 .. Sqrt (Natural'Last / 2)   <=>   0 .. 32767
--
--  Of course, this bound is quite conservative, but it may be enough for a
--  given application.
--
--  The post-condition can be used to prove the trivial equality as stated
--  in your question.

subtype Domain is Natural range 0 .. 32767;

function Inefficient_Euler_1_Sum_2 (N : Domain) return Natural
with Post => (if N = 0 then Inefficient_Euler_1_Sum_2'Result = 0);
end Testing;

测试.adb

package body Testing with SPARK_Mode  is
-------------------------------
-- Inefficient_Euler_1_Sum_2 --
-------------------------------

function Inefficient_Euler_1_Sum_2 (N : Domain) return Natural is
Sum: Natural := 0;
begin

for I in 0 .. N loop

if I mod 3 = 0 then
Sum := Sum + I;
end if;
if I mod 5 = 0 then
Sum := Sum + I;
end if;
if I mod 15 = 0 then
Sum := Sum - I;
end if;

--  Changed slightly since initial post, no effect on Domain.
pragma Loop_Invariant (Sum <= (2 * I) * I);

end loop;

return Sum;

end Inefficient_Euler_1_Sum_2;
end Testing;

main.adb

with Testing; use Testing;
procedure Main with SPARK_Mode is
begin
pragma Assert (Inefficient_Euler_1_Sum_2 (0) = 0);   
end Main;

输出

$ gnatprove -Pdefault.gpr -j0 --level=1 --report=all
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
main.adb:5:19: info: assertion proved
testing.adb:13:15: info: division check proved
testing.adb:14:24: info: overflow check proved
testing.adb:16:15: info: division check proved
testing.adb:17:24: info: overflow check proved
testing.adb:19:15: info: division check proved
testing.adb:20:24: info: overflow check proved
testing.adb:20:24: info: range check proved
testing.adb:23:33: info: loop invariant preservation proved
testing.adb:23:33: info: loop invariant initialization proved
testing.adb:23:42: info: overflow check proved
testing.adb:23:46: info: overflow check proved
testing.ads:17:19: info: postcondition proved
Summary logged in /obj/gnatprove/gnatprove.out