如何在 Ada 中对 2D 数组类型作为参数的函数进行算术合约运算-解网

问：

我有一个函数，应该返回找到的岛屿计数。
我将这个函数命名为 Count_Islands 它接受一个参数 Map 类型的Map_Array，其中 Map 是 Islands 数组。
Islands 是一种枚举器类型，其中包含 Land、Water。
我在 .ads 中有函数规范，正文在。亚行
我现在面临的问题是如何证明我的函数 Count_Islands'Result 将小于（X * Y）
我试过了： with post => Count_Islands'Result < X * Y -- 每当我运行证明我得到的一切时： medium： post条件可能失败无法证明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。但是GNATproven无法证明我的初始代码来分析这一点，使用Post => Count_Islands'Result < X * Y;

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

ADA 代码-合同 gaps-and-islands spark-ada

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 中对 2D 数组类型作为参数的函数进行算术合约运算

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

评论

评论