dafny - 在 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所有先前的节点。我想知道是否可以实现append dafny 中的复杂度为 O(1)(除了 Ghost 方法)，否则我们需要删除 Valid并使用decreases * ？

谢谢:)

Answer 1

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