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

Question

在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 (除了ghost方法)，或者我们需要删除Valid并使用decreases *

谢谢您：)

Answer 1

footprint是一个ghost变量，因此仅供验证器使用(根据定义，function也是ghost )。它不会被编译和执行，所以你在(运行时)复杂性分析中不必考虑它。