无法证明 Ada Spark 中看似微不足道的平等 [英] Can't prove seemingly trivial equality in Ada Spark

问题描述

所以我有这两个文件.

testing.ads

testing.ads

package Testing with
   SPARK_Mode
is

   function InefficientEuler1Sum2 (N: Natural) return Natural;

   procedure LemmaForTesting with
     Ghost,
     Post => (InefficientEuler1Sum2(0) = 0);

end Testing;

和 testing.adb

and 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 时 ->证明文件，我收到这样的消息:

When I run SPARK -> Prove File, I get such message:

GNATprove
    E:\Ada\Testing SPARK\search\src\testing.ads
        10:14 medium: postcondition might fail
           cannot prove InefficientEuler1Sum2(0) = 0

为什么会这样?我误解了什么或者做错了什么?提前致谢.

Why is that so? What I have misunderstood or maybe done wrong? Thanks in advance.

推荐答案

为了证明平凡等式，您需要确保它被函数的后置条件覆盖.如果是这样，您可以使用简单的 Assert 语句证明相等性，如下例所示.此时不需要引理.

To prove the trivial equality, you need to make sure it is covered by the function's post-condition. If so, you can prove the equality using a simple Assert statement as shown in the example below. No lemma is needed at this point.

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

However, a post-condition is not enough to prove the absence of runtime errors (AoRTE): given the allowable input range of the function, the summation may, for some values of N, overflow. To mitigate the issue, you need to bound the input values of N and show the prover that the value for Sum remains bounded during the loop using a loop invariant (see here, here and here for some background information on loop invariants). For illustration purposes, I've chosen a conservative bound of (2 * I) * I, which will severely restrict the allowable range of input values, but does allow the prover to proof the absence of runtime errors in the example.

testing.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;

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;

ma​​in.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

这篇关于无法证明 Ada Spark 中看似微不足道的平等的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！