Dafny linked queue implementation

Question

I'm following Leino's paper "Specification and verification of OO software" and trying to implement the queue example. I'm unable to resolve an (syntax?) error that comes while defining the valid predicate in the Queue class.

My code looks like this:

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

    var tailContents: seq<int>
    var footprint: set<object>

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

    constructor()
        modifies this
        ensures valid() && fresh(footprint - {this})
        ensures next == null
    {
        next := null;
        tailContents := [];
        footprint := {this};
    }
}

class Queue {
    var head: Node?
    var tail: Node?

    var contents: seq<int>
    var footprint: set<object>
    var spine: set<Node>

    predicate valid()
        reads this, footprint
    {
        this in footprint && spine <= footprint &&
        head != null && head in spine &&
        tail != null && tail in spine &&
        tail.next == null && 
        (forall n | n in spine :: n != null && n.valid())
.......
    }

I get an error

Insufficient reads clause to invoke function

at n.valid(). I'm unsure if this is a syntax error or there is something I'm missing. I know that the paper is quite old and there may be some changes required to the code.

Answer 1

I think there is condition missing in valid predicate of Queue. That is node footprint is subset of queue footprint. In original version, Queue class can only read objects from its footprint. But then it calls node valid predicate where it need to read node footprint. Unless we say that Queue class can read node footprints it will complain. But here solution is simpler as node footprint will be subset of Queue footprint.

predicate valid()
    reads this, footprint
{
    this in footprint && spine <= footprint &&
    head != null && head in spine &&
    tail != null && tail in spine &&
    tail.next == null &&
    (forall n | n in spine :: n.footprint <= footprint) &&
    (forall n | n in spine :: n.valid())
}

---

Edit : Paper also has this in its valid, I think you have missed it