GNATprove: "postcondition might fail" in simple function

Question

I want to write a simple function that finds the biggest number in given Integer array. Here is specification:

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;

And here is function's body:

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;

And when I try to prove this function with SPARK, it says that postcondition might fail. I'm trying to understand this for like 5 hours now and I have no idea why it says so. It's really annoying, this function MUST work. Do you have any idea why SPARK behaves so strange? What is a data example for this function to not fullfil its postcondition? It always returns a value taken directly from given array and it is always maximal.

Answer 1

Your mistake is to make a loop invariant, which is weaker than the postcondition:

Specification:

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;

Implementation:

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 file:

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