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

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

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 ведет себя так странно? Каков пример данных для этой функции, чтобы не выполнить свое постусловие? Он всегда возвращает значение, взятое непосредственно из заданного массива, и оно всегда максимальное.


ada formal-verification gnat spark-ada spark-2014
person Android developer    schedule 22.10.2015    source источник
comment
Обратите внимание, что gnatprove говорит «может». Это не значит, что у него есть контрпример. Это означает только то, что он не может доказать, что постусловие выполнено.   -  person Jacob Sparre Andersen    schedule 23.10.2015

Ответы (1)


arrow_upward
3
arrow_downward

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

Технические характеристики:

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;
person Jacob Sparre Andersen    schedule 23.10.2015
comment
Да, да, спасибо! Я все равно понял это через несколько часов после того, как задал этот вопрос, но я рад видеть, что кто-то действительно дает хороший ответ (у меня было около 5 просмотров через 3 часа после публикации этого вопроса). Между прочим, эти сообщения СПАРКа вводят в заблуждение. - person Android developer; 24.10.2015
comment
Обычно я просматриваю вопросы только тогда, когда получаю ежедневную сводку новых вопросов, поэтому получение ответа до истечения 24 часов — это быстро. - person Jacob Sparre Andersen; 24.10.2015