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/* ファイルのどこで詳細情報を探すべきかわからないことにも注意してください。実際、私にとっての主な困難は、証明者が何を必要としているのかを理解することです。以上のことについて、何かご指摘がありましたら幸いです。