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

将此规格用于Append_Item并不能证明Used_Items等于列表中已使用元素的数量，但是（删除raise Program_Error时）它至少会prove。

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);