如何在 Ada 中对以二维数组类型为参数的函数执行算术契约运算

Question

我有一个函数应该 return 找到的岛屿数。
我将此函数命名为 Count_Islands，它接受一个参数 Map_Array类型为Map，其中Map为Islands数组。
Islands 是一个包含 Land、Water 集的枚举器类型。
我在 .ads 中有功能说明，在 .adb
我现在面临的问题是如何证明我的函数 Count_Islands'结果会小于(X * Y)
我试过：with post => Count_Islands'Result < X * Y -- 每当我运行证明我得到的一切时：中等： post 条件可能 fail 无法证明 Count_Islands'结果 < X * Y

.ads 中的函数：

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:

我希望找到一个 Islands(Lands) 的输出结果是 1，它小于 4 * 5。但是 GNATprove 无法证明我的初始代码来分析它，使用 Post => Count_Islands'结果 < X * Y;

有没有更好的方法来证明这个算法？谢谢你的帮助。

Answer 1

由于例子不完整，冒昧修改了一下。您可以通过添加循环不变量来证明 post 条件。下面的程序在 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;

如何在 Ada 中对以二维数组类型为参数的函数执行算术契约运算

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

ada

code-contracts

gaps-and-islands

spark-ada