SPARK 整数溢出检查 [英] SPARK Integer overflow check

问题描述

我有以下程序:

procedure Main with SPARK_Mode is
   F : array (0 .. 10) of Integer := (0, 1, others => 0);
begin
   for I in 2 .. F'Last loop
      F (I) := F (I - 1) + F (I - 2);
   end loop;
end Main;

如果我运行 gnatprove，我会得到以下结果，指向 + 符号:

If I run gnatprove, I get the following result, pointing to the + sign:

中:溢出检查可能会失败

medium: overflow check might fail

这是否意味着 F (I - 1) 可以等于 Integer'Last，并且添加任何内容都会溢出?如果是这样，那么从程序的流程中是不是很清楚这是不可能的?或者我需要在合同中指定这一点吗?如果不是，那是什么意思?

Does this mean that F (I - 1) could be equal to Integer'Last, and adding anything to that would overflow? If so, then is it not clear from the flow of the program that this is impossible? Or do I need to specify this with a contract? If not, then what does it mean?

一个反例表明在这种情况下gnatprove确实担心Integer的边缘:

A counterexample shows that indeed gnatprove in this case worries about the edges of Integer:

中:溢出检查可能会失败(例如，当 F = (1 => -1, others => -2147483648) 和 I = 2 时)

medium: overflow check might fail (e.g. when F = (1 => -1, others => -2147483648) and I = 2)

推荐答案

这已经是一个老问题了，但我还是想添加一个答案(仅供将来参考).

This is already an old question, but I would like to add an answer anyway (just for future reference).

随着证明者的进步，问题中所述的例子现在在 GNAT CE 2019 中证明是开箱即用的(即不需要循环不变式).还可以证明一个更高级的例子:

With the advancement of provers, the example as stated in the question now proves out-the-box in GNAT CE 2019 (i.e. no loop invariant needed). A somewhat more advanced example can also be proven:

ma​​in.adb

procedure Main with SPARK_Mode is

   --  NOTE: The theoretical upper bound for N is 46 as
   --
   --              Fib (46)    <    2**31 - 1    <    Fib (47)
   --           1_836_311_903  <  2_147_483_647  <  2_971_215_073

   --  NOTE: Proved with Z3 only. Z3 is pretty good in arithmetic. Additional
   --        options for gnatprove:
   --
   --           --prover=Z3 --steps=0 --timeout=10 --report=all

   type Seq is array (Natural range <>) of Natural;

   function Fibonacci (N : Natural) return Seq with
     Pre  =>  (N in 2 .. 46),
     Post =>  (Fibonacci'Result (0) = 0)
     and then (Fibonacci'Result (1) = 1)
     and then (for all I in 2 .. N =>
                Fibonacci'Result (I) = Fibonacci'Result (I - 1) + Fibonacci'Result (I - 2));

   ---------------
   -- Fibonacci --
   ---------------

   function Fibonacci (N : Natural) return Seq is
      F : Seq (0 .. N) := (0, 1, others => 0);
   begin

      for I in 2 .. N loop

         F (I) := F (I - 1) + F (I - 2);

         pragma Loop_Invariant
           (for all J in 2 .. I =>
              F (J) = F (J - 1) + F (J - 2));

         --  NOTE: The loop invariant below helps the prover to proof the
         --        absence of overflow. It "reminds" the prover that all values
         --        from iteration 3 onwards are strictly monotonically increasing.
         --        Hence, if absence of overflow is proven in this iteration,
         --        then absence is proven for all previous iterations.

         pragma Loop_Invariant
           (for all J in 3 .. I =>
              F (J) > F (J - 1));

      end loop;

      return F;

   end Fibonacci;

begin
   null;
end Main;

这篇关于SPARK 整数溢出检查的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！