Dafny中链表指定位置插入节点的验证问题求助

经过多次讨论与尝试，该问题仍未解决。

背景说明 #

• 遵循Rustan Lieno的论文实现链表追加操作后，为验证对相关概念的理解，尝试实现指定位置插入节点的功能，目标是证明命令式类C代码的两个性质：（1）可终止；（2）保持队列的有效性。
• 借助相关资料，终止性已轻松证明，但队列有效性的验证遇到阻碍。

核心难点 #

插入节点时必须更新所有前置节点的footprint：

• 在Lieno的论文中，追加操作通过简单的forall循环即可完成更新，因为最后一个节点可被所有前置节点访问到。
• 但在中间位置插入时，同样需要更新所有前置节点的footprint，现有代码尝试用类似的forall循环实现，但未达到预期效果。

代码实现 #

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(); */
    }
}

当前问题与尝试 #

• 现有代码中curr.valid()断言成立，但node.valid()断言失败。
• 尝试用forall循环更新所有不在当前节点footprint中的前置节点的footprint，还添加过如下额外循环，但均无效果：

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

• 推测需要编写引理说明链表中哪些内容被修改、哪些未被修改，但无法构建该引理，恳请帮助解决。

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