InefficientEuler1Sum と InefficientEuler1Sum2 の 2 つの関数があります。両方が同等であることを証明したい (同じ入力に対して同じ出力)。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;