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

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

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

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

我希望这有帮助，

最好的祝福，