在链表中的随机位置插入节点：Dafny

Question

在SO和Dafny讨论区多次尝试和讨论后，问题仍然没有解决。

Primer：在按照 Rustan Lieno 的论文实现了一个简单的附加操作后，我决定看看我是否正确理解了这些概念，并尝试在给定位置插入一个节点而不是附加。这个想法是为了证明命令式 C 代码 (1) 终止并且 (2) 保留队列的有效性。由于这篇post，终止很容易被证明。

问题是，当一个节点被添加到队列中时，所有前面节点的足迹必须被更新。在 Lieno 的论文中，这是使用简单的 forall 循环来实现的。这已经足够了，因为最后一个节点可以从“所有”先前的节点到达。如果在中间插入节点，我们也必须更新所有先前节点的足迹。我下面的代码尝试使用类似的 forall 循环来做到这一点。 在Dafny讨论区讨论后，有人建议由于信息丢失，我最好使用序列作为我的表示，但尝试没有验证。我暂停了该代码的工作一两天，然后返回到 Lieno 的论文并使用该论文中的谓词。我的尝试如下：

class Node {
    var data: int
    var next: Node?

    ghost var footprint: set<object>

    ghost predicate valid()
        reads this, footprint
    {
        this in footprint &&
        (next != null ==> next in footprint && next.footprint <= footprint && 
            this !in next.footprint)
    }

    constructor(d: int)
        modifies this
        ensures valid() && fresh(footprint - {this})
        ensures next == null && data == d
    {
        data := d;
        next := null;
        footprint := {this};
    }
}

class Queue {
    var head: Node

    ghost var footprint: set<object>
    ghost var spine: set<Node>

    /* opaque */ ghost predicate valid()
        reads this, footprint
    {
        this in footprint && spine <= footprint &&
        head != null && head in spine &&
        (forall n: Node? | n in spine :: n != null && n.footprint <= footprint && n.valid()) &&
        (forall n | n in spine :: n.next != null ==> n.next in spine)
    }

    constructor()
        modifies this
        ensures valid() && fresh (footprint - {this})
    {
        /* reveal valid(); */
        var n := new Node(0);
        head := n;
        footprint := {this} + n.footprint;
        spine := {n};
    }

    method {:vcs_split_on_every_assert} {:rlimit 200} enqueue (d: int, pos: nat)
        requires valid()
        requires 0 <= pos < |spine|
        modifies footprint
        ensures valid() 
        ensures fresh(footprint - old(footprint))
    {
        var curr: Node := head;
        var i: nat := 0;
        /* reveal valid(); */

        while(i < pos && curr.next != null)
            invariant curr in spine
            invariant curr.footprint <= footprint
            invariant curr.next != null ==> curr.next in spine && curr !in curr.next.footprint &&
                curr.next.footprint <= curr.footprint
            invariant curr.valid()
            invariant valid()
            decreases if curr != null then curr.footprint else {}
        {
            curr := curr.next;
            i := i + 1;
        }

        assert /* {:only} */ forall m: Node | m in spine && m in curr.footprint :: m.valid();

        var node: Node := new Node(d);
        node.next := curr.next;
        node.footprint := node.footprint + curr.footprint - {curr};
        spine := spine + {node};
        curr.next := node;
        curr.footprint := curr.footprint + node.footprint;
        assert curr.valid();
        assert node.valid();

        forall m | m in spine && m !in curr.footprint {
            /* we update all those nodes that are not a part of the footprint of the current node. 
            As per the updates above, these nodes are all those nodes which current node cannot reach
            i.e., the preceding nodes. */
            m.footprint := m.footprint + curr.footprint;
        }

        footprint := footprint + node.footprint;

        /* assert forall m | m in spine && m !in node.footprint :: m.valid(); */
    }
}

现在，

cure.valid()

成立。但是

node.valid()

失败了。 forall 用于更新所有先前节点的足迹。我们的理解是，所有那些“不”在当前节点足迹中的节点的足迹将被更新。我认为，更新脊柱中的单个节点会破坏脊柱中所有节点的有效性。所以我添加了另一个 forall 循环，例如：

forall m | m in spine && m !in curr.footprint && m.next != null  {
    m.footprint := m.footprint + m.next.footprint;
}

但无济于事。

我认为可能需要一个引理来说明脊柱中发生了什么变化和没有发生什么变化，但我无法构建这样的引理。

非常感谢任何解决此问题的帮助！

现在，cure.valid()成立。但是 node.valid() 失败了。

Answer 1

这是失败的，因为 Dafny 不知道该节点是新分配的节点，而不是一些已经使用的节点。

您错过了在节点构造函数中添加

ensures fresh({this})

，就像您为队列构造函数所做的那样。添加此后

node.valid

进行验证。