adaformal-verificationspark-adaspark-formal-verification

GNATprove: "postcondition might fail" in simple function


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.


Solution

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