4

我有以下程序：

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，我会得到以下结果，指向+标志：

中：溢出检查可能会失败

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

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

medium：溢出检查可能会失败（例如 whenF = (1 => -1, others => -2147483648)和I = 2）

4

3 回答 3

2

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

随着证明者的进步，问题中所述的示例现在在 GNAT CE 2019 中证明是开箱即用的（即不需要循环不变量）。还可以证明一个更高级的示例：

主文件

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;
于 2019-07-23T17:53:12.993 回答
2

考虑为您的代码添加循环不变量。以下是《使用 Spark 构建高完整性应用程序》一书中的示例。

procedure Copy_Into(Buffer : out Buffer_Type;
                    Source : in String) is
   Characters_To_Copy : Buffer.Count_Type := Maximum_Buffer_Size;
begin
   Buffer := (Others => ' '); -- Initialize to all blanks
   if Source'Length < Characters_To_Copy then
      Characters_To_Copy := Source'Length;
   end if;
   for Index in Buffer.Count_Type range 1..Characters_To_Copy loop
      pragma Loop_Invariant
        (Characters_To_Copy <= Source'Length and
         Characters_To_Copy = Characters_To_Copy'Loop_Entry);
      Buffer (Index) := Source(Source'First + (Index - 1));
   end loop;
end Copy_Into;
于 2017-11-10T17:37:52.700 回答
1

这个循环不变量应该有效 - 因为 2^(n-1) + 2^(n-2) < 2^n - 但我无法说服证明者：

procedure Fibonacci with SPARK_Mode is
   F : array (0 .. 10) of Natural := (0      => 0,
                                      1      => 1,
                                      others => 0);
begin
   for I in 2 .. F'Last loop
      pragma Loop_Invariant
        (for all J in F'Range => F (J) < 2 ** J);

      F (I) := F (I - 1) + F (I - 2);
   end loop;
end Fibonacci;

您可能可以通过一些手动帮助来说服证明者（显示 2^(n-1) + 2^(n-2) = 2^(n-2) * (2 + 1) = 3/4 * 2 ^n < 2^n)。

于 2017-11-14T08:30:53.133 回答