ada - SPARK 中的程序验证 - 计算数组中的元素

Question

我写了一个非常简单的程序，但我未能证明它的功能正确性。它使用一个项目列表，每个项目都有一个字段指示它是免费的还是使用过的：

   type t_item is record
      used  : boolean := false; 
      value : integer   := 0;
   end record;

   type t_item_list is array (1 .. MAX_ITEM) of t_item;
   items       : t_item_list;

还有一个计数器指示使用的元素数量：

  used_items  : integer   := 0;

append_item过程检查used_items计数器以查看列表是否已满。如果不是，则第一个空闲条目被标记为已使用，并且used_items计数器递增：

   procedure append_item (value : in  integer; success : out boolean)
   is
   begin

      if used_items = MAX_ITEM then
         success := false;
         return;
      end if;

      for i in items'range loop
         if not items(i).used then
            items(i).value := value;
            items(i).used  := true;
            used_items     := used_items + 1;
            success := true;
            return;
         end if;
      end loop;

      -- Should be unreachable
      raise program_error;
   end append_item;

我不知道如何证明used_items等于列表中已使用元素的数量。另请注意，gnatprove 消息有时令人费解，我不知道在哪里可以在许多 gnatprove/* 文件中查找更多信息。事实上，对我来说主要的困难是弄清楚证明者需要什么。如果你对这一切有一些迹象，我会很高兴。

score 5 · Accepted Answer

计算数据结构中具有给定属性的元素确实很难表达。为了帮助解决这个问题，我们在引理库中提供了通用计数函数的 SPARK pro。用户指南中描述了这个高级函数库：

http://docs.adacore.com/spark2014-docs/html/ug/en/source/spark_libraries.html#higher-order-function-library

要使用它，您应该修改您的项目文件以使用引理库的项目文件并将 SPARK_BODY_MODE 设置为 Off。

您还应该将环境变量 SPARK_LEMMAS_OBJECT_DIR 设置为要在其中创建引理库的编译和验证工件的对象目录的绝对路径。

然后，您可以为您的目的实例化 SPARK.Higher_Order.Fold.Count。它需要一个不受约束的数组类型和一个函数来选择应该计算哪些元素。因此，我重写了您的代码以提供此信息并实例化泛型，如下所示：

   type t_item_list_b is array (positive range <>) of t_item;
   subtype t_item_list is t_item_list_b (1 .. MAX_ITEM);

   function Is_Used (X : t_item) return Boolean is
     (X.used);

   package Count_Used is new SPARK.Higher_Order.Fold.Count
     (Index_Type => Positive,
      Element    => t_item,
      Array_Type => t_item_list_b,
      Choose     => Is_Used);

Count_Used 现在包含：

可以在不变量中使用的 Count 函数：

function invariant return boolean is
    (used_items = Count_Used.Count (items));

用于证明计数的常用事物的引理： Count_Zero 证明 count 的结果为 0 是数组中没有元素具有该属性，而 Update_Count 用于知道在更新数组时如何修改 Count。这些性质对人来说是显而易见的，但实际上它们需要归纳来证明，因此它们通常是自动求解器无法达到的。为了证明 append_item，我现在只需要在 item 更新后调用 Update_Count，如下所示：

procedure append_item
 (value    : in  integer;
  success  : out boolean)
 with ...
is
  Old_Items : t_item_list := items with Ghost;
begin

  if used_items = MAX_ITEM then
     success := false;
     return;
  end if;

  for i in items'range loop
     if not items(i).used then
        items(i).value := value;
        items(i).used  := true;
        used_items     := used_items + 1;
        success := true;
        Count_Used.Update_Count (items, Old_Items, I);
        return;
     end if;
  end loop;

  -- Should be unreachable
  raise program_error;
end append_item;

我希望这有帮助，

此致，

score 3 · Accepted Answer

我喜欢 Simons 的方法，我认为它接近于工作。

我以此为起点，应用了一些我能够使用 SPARK 社区版证明的更改，而无需额外的支持包。

我做的第一件事就是利用 Ada 更强大的类型来尽可能地限制类型。特别是，我没有将 Used_Items 定义为 Integer，而是定义了一个 Element_Count 子类型，其范围不能超过 Max_Items。您应用此类约束越多，您需要传递给证明者的工作就越少。

然后我创建了一个 Integer_List 类型作为更高级别的抽象类型，并将数组类型和元素类型移动到包的私有部分。

这样做，我发现简化了界面，我想。因为创建辅助函数（Length 和 Is_Full）是有意义的，它们在先决条件中用于更简单地向客户端表达属性，这很有帮助，因为它们在前置条件和后置条件中重复多次，但在包的私有部分更具体地提供细节。我在前置条件和后置条件中使用了条件表达式，因为我认为这更清楚地向读者表达了合同。

我发现我需要添加的唯一另一件事是 Append_Item 主体中的循环不变量。证明者告诉我，我错过了一个循环不变量，我添加了它。你基本上需要证明你不能退出循环而不陷入 if 语句找到一个插槽来添加新值。

package Array_Item_Lists with SPARK_Mode is

   Max_Item : constant := 3;

   subtype Element_Count is Natural range 0 .. Max_Item;

   type Integer_List is private;

   function Length (List : Integer_List) return Element_Count;

   function Is_Full (List : Integer_List) return Boolean;

   procedure Append_Item (List    : in out Integer_List;
                          Value   : Integer;
                          Success : out Boolean)
     with
       Pre  => (if Length (List) < Max_Item
                      then not Is_Full (List)
                      else Is_Full (List)),
       Post =>
             (if Length (List'Old) < Max_Item
              then Length (List) = Length (List'Old) + 1
              and then Success 
             else (Length (List'Old) = Max_Item and then Success = False));

private

   type t_item is record
      used  : Boolean := False; 
      value : Integer   := 0;
   end record;

   type t_item_list is
     array (Element_Count range 1 .. Element_Count'Last) of t_item;

   type Integer_List is
      record
         Items : t_item_list;
         used_items : Element_Count := 0;
      end record;

   function Length (List : Integer_List) return Element_Count is
      (List.used_items);

   function Is_Full (List : Integer_List) return Boolean is
      (for all Item of List.Items => Item.used);

end Array_Item_Lists;


pragma Ada_2012;
package body Array_Item_Lists with SPARK_Mode is

   procedure Append_Item (List    : in out Integer_List;
                          Value   : Integer;
                          Success : out Boolean) is
   begin

      Success := False;

      if List.used_items = Max_Item then
         return;
      end if;

      for i in List.Items'Range loop

         pragma Loop_Invariant
           (for some j in i .. Max_Item => not List.Items (j).used);

         if not List.Items (i).used then
            List.Items (i).value := Value;
            List.Items (i).used  := True;
            List.used_items     := List.used_items + 1;
            Success := True;
            return;
         end if;
      end loop;

   end Append_Item;

end Array_Item_Lists;

score 3 · Accepted Answer

使用这个规范Append_Item并不能证明它Used_Items等于列表中使用的元素的数量，但是（去掉raise Program_Error）它至少证明了.

procedure Append_Item (Value : in  Integer; Success : out Boolean)
with Pre =>
  Used_Items <= Max_Item  -- avoid overflow check
  and
  (Used_Items = Max_Item
   or (for some Item of Items => not Item.Used)),
  Post =>
    (Used_Items'Old < Max_Item
     and Used_Items = Used_Items'Old + 1
     and Success = True)
    or (Used_Items'Old = Max_Item and Success = False);

score 1 · Accepted Answer

这个版本有更多的工作，并且可能可以改进，但它试图证明更多的功能属性可能希望应用于这个问题。例如，它确保将一个元素添加到列表中只修改一个存储元素，而不会修改其他存储元素，并且列表中的元素数与数组中已使用的插槽数相匹配。这个版本还提供了一个主程序，它是用 SPARK 编写的，使用该包。

我确实有一个中间版本，我很容易得到它，证明了额外的功能需求，但是当我尝试将它与用 SPARK 编写的客户端程序一起使用时，它导致我添加和修改我所拥有的。

package Array_Item_Lists with SPARK_Mode is

   Max_Item : constant := 3; -- Set to whatever limit is desired

   subtype Element_Count is Natural range 0 .. Max_Item;
   subtype Element_Index is Natural range 1 .. Max_Item;

   type Integer_List is private;

   function Create return Integer_List
     with Post => Length (Create'Result) = 0
       and then Used_Count (Create'Result) = 0
       and then not Is_Full (Create'Result)
       and then Not_Full (Create'Result)
       and then (for all I in 1 .. Max_Item =>
                   not Has_Element (Create'Result, I));

   function Length (List : Integer_List) return Element_Count;
   function Used_Count (List : Integer_List) return Element_Count;

   --  Is_Full is based on Length being = Max_Item
   function Is_Full (List : Integer_List) return Boolean;

   --  Not_Full is based on there being empty slots in the list available
   --  Since the length is kept in sync with number of used slots, the
   --  negation of one result should be equivalent to the result of the other 
   function Not_Full (List : Integer_List) return Boolean;

   function Next_Index (List : Integer_List) return Element_Index
     with Pre => Used_Count (List) = Length (List)
     and then Length (List) < Max_Item and then Not_Full (List),
          Post => not Has_Element (List, Next_Index'Result);

   function Element (List  : Integer_List;
                     Index : Element_Index) return Integer;

   function Has_Element (List  : Integer_List;
                         Index : Element_Index) return Boolean;

   procedure Append_Item (List    : in out Integer_List;
                          Value   : Integer;
                          Success : out Boolean)
   with
     Pre  => Used_Count (List) = Length (List)
        and then (if Length (List) < Max_Item
                   then Not_Full (List) and then
                     not Has_Element (List, Next_Index (List))
                 else Is_Full (List)),
     Post =>
       (if not Is_Full (List) then Not_Full (List)) and then
         (if Length (List'Old) < Max_Item
                  then Success
          and then Length (List) = Length (List'Old) + 1
          and then Element (List, Next_Index (List'Old)) = Value
          and then Has_Element (List, Next_Index (List'Old))
          and then (for all I in 1 .. Max_Item =>
                      (if I /= Next_Index (List'Old) then
                           Element (List'Old, I) = Element (List, I)
                       and then
                         Has_Element (List'Old, I) = Has_Element (List, I)))
          and then Used_Count (List) = Used_Count (List'Old) + 1

           else not Success and then
                Length (List) = Max_Item and then List'Old = List
         and then Used_Count (List) = Max_Item);

private

   type t_item is record
      Used  : Boolean := False; 
      Value : Integer   := 0;
   end record;

   type t_item_list is
     array (Element_Count range 1 .. Element_Count'Last) of t_item;

   type Integer_List is
      record
         Items      : t_item_list := (others => (Used => False, Value => 0));
         Used_Items : Element_Count := 0;
      end record;

   function Element (List  : Integer_List;
                     Index : Element_Index) return Integer is
     (List.Items (Index).Value);

   function Has_Element (List  : Integer_List;
                         Index : Element_Index) return Boolean is
      (List.Items (Index).Used);

   function Length (List : Integer_List) return Element_Count is
      (List.Used_Items);

   function Is_Full (List : Integer_List) return Boolean is
     (for all Item of List.Items => Item.Used
      and then Length (List) = Max_Item);

   function Not_Full (List : Integer_List) return Boolean is
     (for some Item of List.Items => not Item.Used
      --  Used_Count (List) < Max_Item
     );

end Array_Item_Lists;

我对同时拥有 Is_Full 函数和 Not_Full 函数不太满意，这可能是可以简化的事情。但是，一旦我在下面的正文中添加了一些合理的假设，我确实设法证明了这一点。

pragma Ada_2012;
package body Array_Item_Lists with SPARK_Mode is

   procedure Append_Item (List    : in out Integer_List;
                          Value   :        Integer;
                          Success : out    Boolean)
   is
      Old_Used_Count : constant Element_Count := Used_Count (List);
   begin

      if List.Used_Items = Max_Item then
         Success := False;
         return;
      end if;

      declare
         Update_Index : constant Element_Index := Next_Index (List);
      begin

         pragma Assert (List.Items (Update_Index).Used = False);

         List.Items (Update_Index) := (Value => Value, Used => True);
         List.Used_Items     := List.Used_Items + 1;
         Success := True;
         pragma Assert (List.Items (Update_Index).Used = True);

         --  We have proven that one the one element of the array
         --  has been modified, and that it was previous not used,
         --  and that not it is used. From this, we can now assume that
         --  the use count was incremented by one
         pragma Assume (Used_Count (List) = Old_Used_Count + 1);

         --  If the length isn't full (Is_Full) we can assume the
         --  number of used items has room also. We incremented both
         --  of these above, and the two numbers are always in sync.
         pragma Assume (if not Is_Full (List) then Not_Full (List));

      end;

   end Append_Item;

   -----------------------------------------------------------------

   function Create return Integer_List is
      Result : Integer_List := (Items => <>,
                                Used_Items => 0);
   begin

      for I in Result.Items'Range loop         
         Result.Items (I) := (Used => False, Value => 0);

         pragma Loop_Invariant
           (for all J in 1 .. I => Result.Items (J).Used = False);

      end loop;

      pragma Assert (for all Item of Result.Items => Item.Used = False);

      --  Since we have just proven that all items are not used, we know
      --  the Used_Count has to be zero, and hence we are not full
      --  so we can make the following assumptions
      pragma Assume (Used_Count (Result) = 0);
      pragma Assume (Not_Full (Result));

      return Result;
   end Create;

   -----------------------------------------------------------------

   function Next_Index (List : Integer_List) return Element_Index
   is
      Result : Element_Index := 1;
   begin

      Search_Loop :
      for I in List.Items'Range loop

         pragma Loop_Invariant
            (for some J in I .. Max_Item => not List.Items (J).Used);

         if not List.Items (I).Used then
            Result := I;
            exit Search_Loop;
         end if;
      end loop Search_Loop;

      return Result;
   end Next_Index;

   function Used_Count (List : Integer_List) return Element_Count is
      Count : Element_Count := 0;
   begin
      for Item of List.Items loop
         if Item.Used then
            Count := Count + 1;
         end if;
      end loop;

      return Count;
   end Used_Count;

end Array_Item_Lists;

最后，这是一个调用上述包的 SPARK 主程序

with Ada.Text_IO; use Ada.Text_IO;
with Array_Item_Lists;

procedure Main with SPARK_Mode
is
   List : Array_Item_Lists.Integer_List := Array_Item_Lists.Create;
   Success : Boolean;
begin

   Array_Item_Lists.Append_Item (List    => List,
                                 Value   => 3,
                                 Success => Success);

   pragma Assert (Success);

   Array_Item_Lists.Append_Item (List    => List,
                                 Value   => 4,
                                 Success => Success);

   pragma Assert (Success);

   Array_Item_Lists.Append_Item (List    => List,
                                 Value   => 5,
                                 Success => Success);

   pragma Assert (Success);

   Array_Item_Lists.Append_Item (List    => List,
                                 Value   => 6,
                                 Success => Success);

   pragma Assert (not Success);

   Put_Line ("List " &
             (if Array_Item_Lists.Is_Full (List)
                then "is Full!" else "has room!"));
end Main;

ada - SPARK 中的程序验证 - 计算数组中的元素

4 回答 4

Related

Reference