How to perform arithmetic contract operations on function taking in 2D array type as parameter in Ada

Question

1. I have a function that should return the count of Islands found.

2. I name this function Count_Islands that takes in a parameter of Map_Array of type Map, of which Map is an array of Islands.

3. Islands is an enumerator type with set of Land, Water.

4. I have the function specification in the .ads and the body in the .adb

5. The problem I face now is how to proof that my function Count_Islands'Result will be less than (X * Y)

6. I have tried: with post => Count_Islands'Result < X * Y -- Whenever I ran prove all I got: medium: postcondition might fail cannot prove Count_Islands'Result < X * Y

Function in .ads:

function Count_Islands(Map_Array : Map) 
    return Integer with Pre => Map_Array'Length /= 0, 
                        Post => Count_Islands'Result < X * Y;

Function in .adb:

function Count_Islands(Map_Array : Map) return Integer
   is
      Visited_Array : Visited := (others => (others=> False));
      Count : Integer := 0;
   begin
      if (Map_Array'Length = 0)then
         return 0;
      end if;
      for i in X_Range loop
         for j in Y_Range loop
            if (Map_Array(i, j) = Land and then not Visited_Array(i,j)) then
               Visited_Array := Visit_Islands(Map_Array, i, j,Visited_Array);
               Count := Count + 1;
            end if;
         end loop;
      end loop;
      return Count;
   end Count_Islands;

In a matrix of 4 * 5 for instance,i.e my X = 4 And Y = 5:

I expect the output result of an Islands(Lands) found to be 1 which is less than 4 * 5. But GNATprove cannot prove my initial code to analyze that,using Post => Count_Islands'Result < X * Y;

Is there any better way to prove this arithmetic? Thanks for your help.

Answer 1

As the example is not complete, I took the liberty to change it a little bit. You can prove the post condition by adding loop invariants. The program below proves in GNAT CE 2019:

main.adb

procedure Main with SPARK_Mode is

   --  Limit the range of the array indices in order to prevent 
   --  problems with overflow, i.e.:
   --
   --     Pos'Last * Pos'Last <= Natural'Last
   --
   --  Hence, as Natural'Last = 2**31 - 1,
   --
   --     Pos'Last <= Sqrt (2**31 - 1) =approx. 46340
   --
   --  If Pos'Last >= 46341, then overflow problems might occur. 

   subtype Pos is Positive range 1 .. 46340;

   type Map_Item is (Water, Land);

   type Map is
     array (Pos range <>, Pos range <>) of Map_Item;

   type Visited is
     array (Pos range <>, Pos range <>) of Boolean;


   function Count_Islands (Map_Array : Map) return Natural with
     Post => Count_Islands'Result <= Map_Array'Length (1) * Map_Array'Length (2);


   -------------------
   -- Count_Islands --
   -------------------

   function Count_Islands (Map_Array : Map) return Natural is

      Visited_Array : Visited (Map_Array'Range (1), Map_Array'Range (2)) :=
        (others => (others => False));

      Count : Natural := 0;

   begin

      for I in Map_Array'Range (1) loop

         pragma Loop_Invariant
           (Count <= (I - Map_Array'First (1)) * Map_Array'Length (2));

         for J in Map_Array'Range (2) loop            

            pragma Loop_Invariant
              (Count - Count'Loop_Entry <= J - Map_Array'First (2));

            if Map_Array(I, J) = Land and then not Visited_Array(I, J) then
               Visited_Array (I, J) := True;   --  Simplified
               Count := Count + 1;
            end if;

         end loop;

      end loop;      

      return Count;

   end Count_Islands;

begin
   null;
end Main;