【发布时间】：2020-11-08 21:25:42
【问题描述】：
我有两个函数：InefficientEuler1Sum 和 InefficientEuler1Sum2。我想证明它们都是等价的（给定相同输入的相同输出）。
当我运行 SPARK -> Prove File（在 GNAT Studio 中）时，我在文件 euler1.adb 中收到关于行 pragma Loop_Invariant(Sum = InefficientEuler1Sum(I)); 的此类消息：
loop invariant might fail in first iterationloop invariant might not be preserved by an arbitrary iteration
似乎（例如，在尝试手动证明时）函数 InefficientEuler1Sum2 不知道 InefficientEuler1Sum 的结构。向它提供这些信息的最佳方式是什么？
文件 euler1.ads：
package Euler1 with
SPARK_Mode
is
function InefficientEuler1Sum (N: Natural) return Natural with
Ghost,
Pre => (N <= 1000);
function InefficientEuler1Sum2 (N: Natural) return Natural with
Ghost,
Pre => (N <= 1000),
Post => (InefficientEuler1Sum2'Result = InefficientEuler1Sum (N));
end Euler1;
文件euler1.adb：
package body Euler1 with
SPARK_Mode
is
function InefficientEuler1Sum(N: Natural) return Natural is
Sum: Natural := 0;
begin
for I in 0..N loop
if I mod 3 = 0 or I mod 5 = 0 then
Sum := Sum + I;
end if;
pragma Loop_Invariant(Sum <= I * (I + 1) / 2);
end loop;
return Sum;
end InefficientEuler1Sum;
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;
pragma Loop_Invariant(Sum <= 2 * I * I);
pragma Loop_Invariant(Sum = InefficientEuler1Sum(I));
end loop;
return Sum;
end InefficientEuler1Sum2;
end Euler1;
【问题讨论】：
-
看来你的两个函数的post条件都不充分。 InefficientEuler1Sum 没有后置条件，并且 InefficientEuler1Sum2 的现有后置条件不将其输入与其输出相关联。只有指定了输出，才能证明这两个函数具有相等的输出。
-
你建议为 InefficientEuler1Sum 写什么样的后置条件？ （让我们假设我不知道它的封闭形式表达式。）也不同意 InefficientEuler1Sum2 的后置条件，因为这里显然有 InefficientEuler1Sum2'Result ......无论如何，我可能是错的......你能，如果可能，说明你将如何证明等价性？
-
鉴于两个函数中的循环不变量，很明显这两个函数通常会产生不同的结果。对于相同的输入值 N，Sum
-
@JimRogers 这不正确。 不清楚“这两个函数通常会产生不同的结果”。循环不变量断言
Sum的值在两个函数中保持低于（或处于）某个界限。他们没有断言Sum的具体值，也没有证明给定输入N的函数的具体结果，除了一个范围。 OP 只是在InefficientEuler1Sum中使用了不同的（不太保守的）界限（基于算术级数，实际上非常好）。