小编Les*_*ess的帖子

所以我有这两个文件。

测试广告

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 …