Dafny中基于动态帧验证的链表能否实现O(1)复杂度的append操作

在Dafny中，我们可以使用set<T>作为动态帧来验证链表的终止性，对应示例代码如下：

class Node {
  // 节点及其后继节点中存储的数据值序列。
  ghost var list: seq<Data>;
  // `footprint`是由当前节点及其后继节点组成的集合，本质是论文中提到的动态帧。
  ghost var footprint: set<Node>;

  var data: Data;
  var next: Node?;

  // 合法（Valid）链表指无环的链表。
  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属性，带来不必要的性能开销。

待解答的技术问题 #

围绕上述实现的效率瓶颈，核心问询包括两点：

• 不借助额外ghost方法的前提下，能否在Dafny中实现时间复杂度为*O(1)*的链表append操作？
• 是不是必须移除原有Valid谓词的约束、改用decreases *完成终止性验证，才能兼顾实现效率？

内容的提问来源于stack exchange，提问作者zhuzilin