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

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())
}
...
}

(这是在面向对象软件的规范和验证中的实现。(

然而，footprint使得难以实现append操作。因为在将新节点追加到链表中时，我们需要更新以前所有节点的footprint。我想知道是否有可能在dafny中实现具有O(1(复杂性的append(除了ghost方法(，或者我们需要删除Valid并使用decreases *？

谢谢：(

Answer 1

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