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 / *文件中从何处查找更多信息。实际上，对我而言，主要困难是弄清楚证明者的需求。如果您对此有任何表示，我将非常高兴。

Answer 1

在数据结构中对具有给定属性的元素进行计数确实很难表达。为了解决这个问题，我们在引理库中提供了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，我现在只需要在项更新之后调用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;
  

我希望这有帮助，

最好的祝福，

Answer 2

使用此规范并Append_Item不能证明 \xe2\x80\x99Used_Items等于列表中已使用元素的数量，但（删除 ）raise Program_Error它至少证明了。

\n\n

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

\n