我有两个函数：InefficientEuler1Sum 和 InefficientEuler1Sum2。我想证明它们都是等价的（给定相同输入的相同输出）。当我运行 SPARK -> Prove File（在 GNAT Studio 中）时，我pragma Loop_Invariant(Sum = InefficientEuler1Sum(I));在文件 euler1.adb 中收到有关行的此类消息：
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;