SPARK Целочисленная проверка переполнения

Question

У меня есть следующая программа:

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:

средний: проверка переполнения может завершиться неудачно (например, когда F = (1 => -1, others => -2147483648) а также I = 2)

Answer 1

Это уже старый вопрос, но я все равно хотел бы добавить ответ (на всякий случай).

С развитием доказывающих, пример, указанный в вопросе, теперь оказывается готовым к использованию в GNAT CE 2019 (т.е. инвариант цикла не требуется). Можно доказать и более сложный пример:

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

Answer 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;

Answer 3

Этот инвариант цикла должен работать - так как 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).