Linked list insertion in Dafny

Question

After following Rustan Leino's paper, I was able to complete the verification of a linked queue. Now, I'm trying to implement a more general insertion in queue, i.e., instead of appending a node, we insert a node at a given position.

After referring a few SO posts, I have come up with the following code:

class Node {
    var data: int
    var next: Node?
    
    ghost var footprint: set<object>
    ghost var contents: seq<int>
    
    ghost predicate valid()
        reads this, footprint
    {
        this in footprint &&
        (next != null ==> next in footprint &&
            next.footprint <= footprint &&
            this !in next.footprint &&
            next.valid()) &&
        (next == null ==> |contents| == 0 &&
            next != null ==> next.contents == contents[1..])
    }
    
    constructor()
        modifies this
        ensures valid() && fresh(footprint - {this})
        ensures next == null
        ensures |contents| == 0
    {
        next := null;
        contents := [];
        footprint := {this}
    }
    
    method enqueueMid(d: int, pos: int)
        requires valid()
        requires 0 <= pos <= |contents|
        modifies footprint
        enures valid() && fresh(footprint - old(footprint))
    {
        var i: int := 0;
        var curr := this;
        
        while(i < pos && curr.next != null)
            invariant curr != null
            invariant curr != null ==> curr.valid()
            decreases if curr != null then curr.footprint else {}
        {
            i := i + 1;
            curr := curr.next;
        }
        
        var n := new Node();
        n.data := d;
        
        if(curr == null) {
            curr := n;
            contents := contents + [d]; // if current is null then we have reached the end of the list!
        } else {
            n.next := curr.next;
            n.footprint := curr.footprint - {curr}; // acyclicity!
            curr.footprint := curr.footprint + n.footprint;
            curr.next := n;
            contents := contents[ .. pos] + [d] + contents[pos ..];
        }
        
        footprint := footprint + n.footprint;
        assert(valid()); // error: could not prove: next in footprint. could not prove: next.valid()
    }
}

The final assertion gives me errors.I think the valid predicate is not well formed. I referred to this SO question to frame my predicate and also the while loop. Moreover, I think, I have to reason about how contents is updated. I cannot figure that out though.

Any help is much appreciated!

Answer 1

This is almost solution (I am using one assumption).

One of major problem I see in your approach is you are only updating footprint and contents of node just before node to be inserted. But this will invalid all previous nodes contents and footprint invariant. That is what I meant when I said (in comments) that you need to roll back to head again fixing footprint and contents of each previous nodes. I have made some small changes in my solution regarding pos precondition and valid predicate.

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

  ghost var contents: seq<int>
  ghost var footprint: set<object>

  ghost predicate valid()
    decreases footprint
    reads this, footprint
  {
     this in footprint &&
     (next != null ==> (next in footprint && next.footprint < footprint && this !in next.footprint)) &&
     (next != null ==> next.valid()) &&
     (next != null ==> contents == [data] + next.contents) &&
     (next == null ==> contents == [data])
  }

  constructor (d: int)
    ensures valid()
    ensures data == d && next == null
  {
     data, next := d, null;
     footprint, contents := {this}, [data];
  }

  method insert(pos: int, d: int)
    requires valid()
    modifies footprint
    requires 0 <= pos < |contents|
    ensures valid()
  {
     var i := 0;
     var curr := this;

     ghost var nodes := [curr];

     while i < pos && curr.next != null
      invariant curr != null
      invariant 1 <= |nodes| && nodes[|nodes|-1] == curr
      invariant curr.valid()
      invariant nodes[0] == this
      invariant curr.footprint <= footprint
      invariant forall j :: 0 <= j < |nodes| ==> nodes[j] != null && nodes[j].valid() && nodes[j] in footprint
      invariant forall j :: 1 <= j < |nodes| ==> nodes[j] == nodes[j-1].next && nodes[j-1] !in nodes[j].footprint
     {
        i, curr := i + 1, curr.next;
        assert curr.valid();
        nodes := nodes + [curr];
     }

     var nn := new Node(d);
     nn.next := curr.next;
     if curr.next != null {
       nn.footprint, nn.contents := {nn} + curr.next.footprint, [d] + curr.next.contents;
     }
     assert nn.valid();
     assert curr in footprint;
     curr.next := nn;
     assert nn in curr.next.footprint;

     var j := |nodes|-1;
     assert nodes[j].next == nn;
     assert nodes[j].next.valid();

     while j >= 0
       invariant 0 <= j < |nodes|
       invariant nodes[0] == this
       invariant forall k : int :: 0 <= j <= k < |nodes| ==> nodes[k].next != null && nodes[k].next.valid()
       invariant forall k : int :: 0 <= j < k < |nodes| ==> nodes[k].valid()
     {
        nodes[j].footprint := {nodes[j]} + nodes[j].next.footprint;
        assert nodes[j].next in nodes[j].next.footprint;
        assert nodes[j] in nodes[j].footprint;
        assume nodes[j].footprint < nodes[j].next.footprint;
        nodes[j].contents := [nodes[j].data] + nodes[j].next.contents;
        j := j - 1;
     }
     assert nodes[0].valid();
  }
}