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

【问题标题】：Program verification in SPARK - Counting elements in an arraySPARK 中的程序验证 - 计算数组中的元素
【发布时间】：2019-11-18 16:28:25
【问题描述】：

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

   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/* 文件中查找更多信息。事实上，对我来说主要的困难是弄清楚证明者需要什么。如果您对这一切有一些迹象，我将非常高兴。

【问题讨论】：

你没有说尝试插入重复值会发生什么（错误？忽略？允许？）

标签： ada spark-ada

【解决方案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 证明计数的结果是 0 是数组中没有元素具有该属性，而 Update_Count 用于知道当数组更新时如何修改 Count。这些性质对人来说是显而易见的，但实际上它们需要归纳来证明，因此它们通常是自动求解器无法实现的。为了证明 append_item，我现在只需要在 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;

希望对你有帮助，

最好的问候，

【讨论】：

CE 2019 中似乎没有引理库。
@SimonWright 引理库也可以在GitHub 上的 SPARK 存储库中找到。

【解决方案2】：

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

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

【讨论】：

感谢您的回答。但是，当连续多次调用 append_item() 时，它不起作用（至少在我的 gnatprove 版本中）。我得到以下输出：“中等：前提条件可能失败，无法证明 Used_Items = Max_Item 或（对于某些 Item of Items => not Item.used）...”
如果有 any 调用 Append_Item，它实际上不起作用。我知道我不应该尝试回答 SPARK 问题。如果你不介意，我会删除答案。

【解决方案3】：

我喜欢 Simons 的方法，我认为它接近于工作。

我以此为起点，应用了一些我能够使用 SPARK 社区版证明的更改，而无需额外的支持包。

我做的第一件事就是利用 Ada 更强大的类型来尽可能地限制类型。特别是，我没有将 Used_Items 定义为 Integer，而是定义了一个 Element_Count 子类型，其范围不能超过 Max_Items。您应用此类约束的次数越多，您需要传递给证明者的工作就越少。

然后我创建了一个 Integer_List 类型作为更高级别的抽象类型，并将数组类型和元素类型移动到包的私有部分。

这样做，我发现简化了界面，我想。因为创建在先决条件中使用的辅助函数（Length 和 Is_Full）是有意义的更简单地向客户表达属性，这很有帮助，因为它们在前置和后置条件中重复了几次，但在包的私有部分中被扩展以更具体地提供细节。我在前置条件和后置条件中使用了条件表达式，因为我认为更清楚地向读者表达合同。

我发现我需要添加的唯一另一件事是主体中的循环不变量 Append_Item 的。证明者告诉我我缺少一个循环不变量，我补充说。你基本上需要证明你不能在没有的情况下退出循环陷入 if 语句中，寻找一个添加新值的槽。

package Array_Item_Lists with SPARK_Mode is

   Max_Item : constant := 3;

   subtype Element_Count is Natural range 0 .. Max_Item;

   type Integer_List is private;

   function Length (List : Integer_List) return Element_Count;

   function Is_Full (List : Integer_List) return Boolean;

   procedure Append_Item (List    : in out Integer_List;
                          Value   : Integer;
                          Success : out Boolean)
     with
       Pre  => (if Length (List) < Max_Item
                      then not Is_Full (List)
                      else Is_Full (List)),
       Post =>
             (if Length (List'Old) < Max_Item
              then Length (List) = Length (List'Old) + 1
              and then Success 
             else (Length (List'Old) = Max_Item and then Success = False));

private

   type t_item is record
      used  : Boolean := False; 
      value : Integer   := 0;
   end record;

   type t_item_list is
     array (Element_Count range 1 .. Element_Count'Last) of t_item;

   type Integer_List is
      record
         Items : t_item_list;
         used_items : Element_Count := 0;
      end record;

   function Length (List : Integer_List) return Element_Count is
      (List.used_items);

   function Is_Full (List : Integer_List) return Boolean is
      (for all Item of List.Items => Item.used);

end Array_Item_Lists;


pragma Ada_2012;
package body Array_Item_Lists with SPARK_Mode is

   procedure Append_Item (List    : in out Integer_List;
                          Value   : Integer;
                          Success : out Boolean) is
   begin

      Success := False;

      if List.used_items = Max_Item then
         return;
      end if;

      for i in List.Items'Range loop

         pragma Loop_Invariant
           (for some j in i .. Max_Item => not List.Items (j).used);

         if not List.Items (i).used then
            List.Items (i).value := Value;
            List.Items (i).used  := True;
            List.used_items     := List.used_items + 1;
            Success := True;
            return;
         end if;
      end loop;

   end Append_Item;

end Array_Item_Lists;

【讨论】：

我发现试图证明一个使用这个包的子程序失败了（列表“未初始化”，后面证明前提条件失败。
我们都没有证明新列表要么包含新元素但其他方面没有改变，要么没有改变。
使用 SPARK，您可以应用不同的注意事项。例如，SPARK 是否应该只应用于系统的某些库？或者应该将其应用于整个系统。在这种情况下，我的假设是 SPARK 仅适用于 Array_Item_Lists 包。
关于您的第二条评论，SPARK 的另一个考虑因素是，如果您想超越消除运行时错误，并证明系统的功能需求，那么您需要决定您需要哪些功能需求想证明。在这种情况下，我只着手证明 Used_Item 计数被正确操作。但是您对想要证明的其他功能特性提出了一些很好的建议。我将提交另一种解决方案，试图解决这些问题，并为想要在 SPARK 中编写整个程序提供更好的支持。

【解决方案4】：

这个版本有更多的工作，并且可能可以改进，但它试图证明更多的功能属性可能想要应用于这个问题。例如，它确保将一个元素添加到列表中只修改一个存储元素，而不会修改其他存储元素，并且列表中的元素数量与数组中使用的插槽数匹配。该版本还提供了一个使用SPARK编写的主程序。

我确实有一个中间版本，我很容易就得到了证明额外的功能要求，但是当我尝试将它与客户端一起使用时用 SPARK 编写的程序，它引导我添加和修改我所拥有的。

package Array_Item_Lists with SPARK_Mode is

   Max_Item : constant := 3; -- Set to whatever limit is desired

   subtype Element_Count is Natural range 0 .. Max_Item;
   subtype Element_Index is Natural range 1 .. Max_Item;

   type Integer_List is private;

   function Create return Integer_List
     with Post => Length (Create'Result) = 0
       and then Used_Count (Create'Result) = 0
       and then not Is_Full (Create'Result)
       and then Not_Full (Create'Result)
       and then (for all I in 1 .. Max_Item =>
                   not Has_Element (Create'Result, I));

   function Length (List : Integer_List) return Element_Count;
   function Used_Count (List : Integer_List) return Element_Count;

   --  Is_Full is based on Length being = Max_Item
   function Is_Full (List : Integer_List) return Boolean;

   --  Not_Full is based on there being empty slots in the list available
   --  Since the length is kept in sync with number of used slots, the
   --  negation of one result should be equivalent to the result of the other 
   function Not_Full (List : Integer_List) return Boolean;

   function Next_Index (List : Integer_List) return Element_Index
     with Pre => Used_Count (List) = Length (List)
     and then Length (List) < Max_Item and then Not_Full (List),
          Post => not Has_Element (List, Next_Index'Result);

   function Element (List  : Integer_List;
                     Index : Element_Index) return Integer;

   function Has_Element (List  : Integer_List;
                         Index : Element_Index) return Boolean;

   procedure Append_Item (List    : in out Integer_List;
                          Value   : Integer;
                          Success : out Boolean)
   with
     Pre  => Used_Count (List) = Length (List)
        and then (if Length (List) < Max_Item
                   then Not_Full (List) and then
                     not Has_Element (List, Next_Index (List))
                 else Is_Full (List)),
     Post =>
       (if not Is_Full (List) then Not_Full (List)) and then
         (if Length (List'Old) < Max_Item
                  then Success
          and then Length (List) = Length (List'Old) + 1
          and then Element (List, Next_Index (List'Old)) = Value
          and then Has_Element (List, Next_Index (List'Old))
          and then (for all I in 1 .. Max_Item =>
                      (if I /= Next_Index (List'Old) then
                           Element (List'Old, I) = Element (List, I)
                       and then
                         Has_Element (List'Old, I) = Has_Element (List, I)))
          and then Used_Count (List) = Used_Count (List'Old) + 1

           else not Success and then
                Length (List) = Max_Item and then List'Old = List
         and then Used_Count (List) = Max_Item);

private

   type t_item is record
      Used  : Boolean := False; 
      Value : Integer   := 0;
   end record;

   type t_item_list is
     array (Element_Count range 1 .. Element_Count'Last) of t_item;

   type Integer_List is
      record
         Items      : t_item_list := (others => (Used => False, Value => 0));
         Used_Items : Element_Count := 0;
      end record;

   function Element (List  : Integer_List;
                     Index : Element_Index) return Integer is
     (List.Items (Index).Value);

   function Has_Element (List  : Integer_List;
                         Index : Element_Index) return Boolean is
      (List.Items (Index).Used);

   function Length (List : Integer_List) return Element_Count is
      (List.Used_Items);

   function Is_Full (List : Integer_List) return Boolean is
     (for all Item of List.Items => Item.Used
      and then Length (List) = Max_Item);

   function Not_Full (List : Integer_List) return Boolean is
     (for some Item of List.Items => not Item.Used
      --  Used_Count (List) < Max_Item
     );

end Array_Item_Lists;

我对同时拥有 Is_Full 函数和 Not_Full 函数不太满意，这可能是可以简化的事情。但是，一旦我在下面的正文中添加了一些合理的假设，我确实设法证明了这一点。

pragma Ada_2012;
package body Array_Item_Lists with SPARK_Mode is

   procedure Append_Item (List    : in out Integer_List;
                          Value   :        Integer;
                          Success : out    Boolean)
   is
      Old_Used_Count : constant Element_Count := Used_Count (List);
   begin

      if List.Used_Items = Max_Item then
         Success := False;
         return;
      end if;

      declare
         Update_Index : constant Element_Index := Next_Index (List);
      begin

         pragma Assert (List.Items (Update_Index).Used = False);

         List.Items (Update_Index) := (Value => Value, Used => True);
         List.Used_Items     := List.Used_Items + 1;
         Success := True;
         pragma Assert (List.Items (Update_Index).Used = True);

         --  We have proven that one the one element of the array
         --  has been modified, and that it was previous not used,
         --  and that not it is used. From this, we can now assume that
         --  the use count was incremented by one
         pragma Assume (Used_Count (List) = Old_Used_Count + 1);

         --  If the length isn't full (Is_Full) we can assume the
         --  number of used items has room also. We incremented both
         --  of these above, and the two numbers are always in sync.
         pragma Assume (if not Is_Full (List) then Not_Full (List));

      end;

   end Append_Item;

   -----------------------------------------------------------------

   function Create return Integer_List is
      Result : Integer_List := (Items => <>,
                                Used_Items => 0);
   begin

      for I in Result.Items'Range loop         
         Result.Items (I) := (Used => False, Value => 0);

         pragma Loop_Invariant
           (for all J in 1 .. I => Result.Items (J).Used = False);

      end loop;

      pragma Assert (for all Item of Result.Items => Item.Used = False);

      --  Since we have just proven that all items are not used, we know
      --  the Used_Count has to be zero, and hence we are not full
      --  so we can make the following assumptions
      pragma Assume (Used_Count (Result) = 0);
      pragma Assume (Not_Full (Result));

      return Result;
   end Create;

   -----------------------------------------------------------------

   function Next_Index (List : Integer_List) return Element_Index
   is
      Result : Element_Index := 1;
   begin

      Search_Loop :
      for I in List.Items'Range loop

         pragma Loop_Invariant
            (for some J in I .. Max_Item => not List.Items (J).Used);

         if not List.Items (I).Used then
            Result := I;
            exit Search_Loop;
         end if;
      end loop Search_Loop;

      return Result;
   end Next_Index;

   function Used_Count (List : Integer_List) return Element_Count is
      Count : Element_Count := 0;
   begin
      for Item of List.Items loop
         if Item.Used then
            Count := Count + 1;
         end if;
      end loop;

      return Count;
   end Used_Count;

end Array_Item_Lists;

最后，这是一个调用上述包的 SPARK 主程序

with Ada.Text_IO; use Ada.Text_IO;
with Array_Item_Lists;

procedure Main with SPARK_Mode
is
   List : Array_Item_Lists.Integer_List := Array_Item_Lists.Create;
   Success : Boolean;
begin

   Array_Item_Lists.Append_Item (List    => List,
                                 Value   => 3,
                                 Success => Success);

   pragma Assert (Success);

   Array_Item_Lists.Append_Item (List    => List,
                                 Value   => 4,
                                 Success => Success);

   pragma Assert (Success);

   Array_Item_Lists.Append_Item (List    => List,
                                 Value   => 5,
                                 Success => Success);

   pragma Assert (Success);

   Array_Item_Lists.Append_Item (List    => List,
                                 Value   => 6,
                                 Success => Success);

   pragma Assert (not Success);

   Put_Line ("List " &
             (if Array_Item_Lists.Is_Full (List)
                then "is Full!" else "has room!"));
end Main;

【讨论】：