在 dafny 中实现链表的追加操作，复杂度为 O(1)

问题描述

在 dafny 中，我们可以使用 set<T> 作为动态框架来验证链表的终止：

class Node {
  // the sequence of data values stored in a node and its successors.
  ghost var list: seq<Data>;
  // `footprint` is a set consisting of the node and its successors.
  // it is actually the dynamic frame mentioned in the paper.
  ghost var footprint: set<Node>;

  var data: Data;
  var next: Node?;

  // A "Valid" linked list is one without ring. 
  function Valid(): bool
    reads this,footprint
  {
    this in footprint &&
    (next == null ==> list  == [data]) &&
    (next != null ==> next in footprint &&
                      next.footprint <= footprint &&
                      !(this in next.footprint) &&
                      list == [data] + next.list &&
                      next.Valid())
  }
  ...
}

（这是 Specification and Verification of Object-Oriented Software 中的实现。）

然而，footprint 使得实现 append 操作变得困难。因为当向链表追加一个新节点时，我们需要更新之前所有节点的footprint。我想知道是否可以在 dafny 中实现复杂度为 O(1) 的 append（幽灵方法除外），或者我们需要删除 Valid 并使用 decreases *？

谢谢:)

解决方法

footprint 是一个 ghost 变量，因此仅由验证者使用（并且 function 根据定义也是 ghost）。它不会被编译和执行，因此您不必在（运行时）复杂性分析中考虑它。

dafny formal-verification