我写了一个非常简单的程序,但未能证明它的功能正确。它使用项目列表,每个项目都有一个字段指示它是免费还是已使用:
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;
我希望这有帮助,
最好的祝福,