1

  1. 我有一个函数应该返回找到的岛屿的数量。

  2. 我将这个函数命名为 Count_Islands，它接收一个 Map 类型的 Map_Array 参数，其中 Map 是一个岛屿数组。

  3. Islands 是一个枚举类型，包含一组 Land、Water。

  4. 我在 .ads 中有函数规范，在 .adb 中有正文

  5. 我现在面临的问题是如何证明我的函数 Count_Islands'Result 将小于 (X * Y)

  6. 我试过：with post => Count_Islands'Result < X * Y -- 每当我跑证明我得到的一切：中等：后置条件可能失败无法证明 Count_Islands'Result < 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：

我希望群岛（土地）的输出结果为 1，小于 4 * 5。但 GNATprove 无法证明我的初始代码来分析它，使用 Post => Count_Islands'Result < X * Y;

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

4

1 回答 1

1

由于示例不完整，我冒昧地对其进行了一些更改。您可以通过添加循环不变量来证明后置条件。以下程序在 GNAT CE 2019 中得到证明：

主文件

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;
于 2019-07-10T21:05:04.203 回答