GNATprove: "постусловие может потерпеть неудачу" в простой функции

Question

Я хочу написать простую функцию, которая находит наибольшее число в данном массиве Integer. Вот спецификация:

package Maximum with SPARK_Mode is

   type Vector is array(Integer range <>) of Integer;

   function Maximum (A : in Vector) return Integer
     with
       SPARK_Mode,
       Pre => A'Length > 0,
         Post =>
         (for all i in A'Range => A(i) <= Maximum'Result)
         and then
           (for some i in A'Range => A(i) = Maximum'Result);

end Maximum;

А вот и тело функции:

package body Maximum with SPARK_Mode is

   function Maximum (A : in Vector) return Integer
   is
   Max : Integer := A (A'First);
   begin
      if (A'Length = 1) then
         return Max;
      end if;

      for I in A'First + 1 .. A'Last loop
         pragma Loop_Invariant
           (for all Index in A'First .. I - 1 => Max >= A(Index));

         if A (I) > Max then
            Max := A (I);
         end if;
      end loop;

      return Max;
   end Maximum;

end Maximum;

И когда я пытаюсь доказать эту функцию с помощью SPARK, он говорит, что постусловие может потерпеть неудачу. Я пытаюсь понять это около 5 часов, и я понятия не имею, почему он так говорит. Это действительно раздражает, эта функция ДОЛЖНА работать. Ты хоть представляешь, почему SPARK ведет себя так странно? Каков пример данных для этой функции, чтобы не выполнить ее постусловие? Он всегда возвращает значение, взятое непосредственно из данного массива, и оно всегда максимально.

Answer 1

Ваша ошибка - сделать цикл инвариантом, который слабее, чем постусловие:

Спецификация:

package Maximum
  with SPARK_Mode
is

   type Vector is array (Integer range <>) of Integer;

   function Maximum (A : in Vector) return Integer
     with
       Pre  => A'Length > 0,
       Post => (for all i in A'Range => A(i) <= Maximum'Result)
               and
               (for some i in A'Range => A(i) = Maximum'Result);

end Maximum;

Реализация:

package body Maximum with SPARK_Mode is

   function Maximum (A : in Vector) return Integer
   is
   Max : Integer := A (A'First);
   begin
      if (A'Length = 1) then
         return Max;
      end if;

      for K in A'First + 1 .. A'Last loop
         pragma Loop_Invariant
           ((for all  I in A'First .. K - 1 => A (I) <= Max)
            and
            (for some I in A'First .. K - 1 => A (I) = Max));

         if A (K) > Max then
            Max := A (K);
         end if;
      end loop;

      return Max;
   end Maximum;

end Maximum;

Файл проекта:

project Maximum is
   for Main use ("maximum");
end Maximum;