GNATprove: «postcondition может сбой» в простой функции

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; 

И когда я пытаюсь доказать эту функцию с СПАРК, он говорит, что Постусловие может потерпеть неудачу. Я пытаюсь понять это примерно через 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;