Как выполнить арифметические контрактные операции при взятии функций в виде двумерного массива в качестве параметра в Ada

Question

1. У меня есть функция, которая должна возвращать количество найденных островов.

2. Я называю эту функцию Count_Islands, которая принимает параметр Map_Array типа Map, из которых Map является массивом островов.

3. острововтип перечислителя с набором Land, Water.

4. У меня есть спецификация функции в .ads и тело в .adb

5. Проблема, с которой я сейчас сталкиваюсь, заключается в том, чтобы доказать, что моя функция Count_Islands'Result будет меньше (X * Y)

6. Я пытался: с post => Count_Islands'Result - Всякий раз, когда я запускаю, докажите, что весь источник, который я получил: medium: postcondition может не получиться, не может доказать Count_Islands'Result

Функция в .adb:

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

Функция в .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;

В матрице 4 * 5, например, то есть мои X = 4 и Y = 5 :

 Map_Array : constant Map := ((Land,  Water, Land, Water, Water),
                                 (Land, Water, Land, Land, Water),
                                 (Land, Water, Land, Land, Water),
                                 (Land, Land, Land, Land, Water));

Я ожидаю, что выходной результат для островов (земель) будет равен 1, который меньше 4 * 5.GNATprove не может доказать моюисходный код для анализа этого, используя Post => Count_Islands'Result

Есть ли лучший способ доказать эту арифметику? Спасибо за вашу помощь.

Answer 1

Поскольку пример не завершен, я позволил себе немного его изменить.Вы можете доказать условие публикации, добавив инварианты цикла.Приведенная ниже программа доказывает в 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;