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.

Can you paste full code. Definition of Node etc are missing

Divyanshu Ranjan
– Divyanshu Ranjan

2024-01-19 13:46:21 +00:00
Commented Jan 19, 2024 at 13:46 — Divyanshu Ranjan
– Divyanshu Ranjan, Commented Jan 19, 2024 at 13:46

Divyanshu Ranjan · Accepted Answer · 2024-01-19 14:09:44Z

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

edited Jan 19, 2024 at 14:09

answered Jan 19, 2024 at 13:57

Divyanshu Ranjan

1,1556 silver badges8 bronze badges

Sign up to request clarification or add additional context in comments.

2 Comments

Drona Nagarajan Over a year ago

Yes, its here in the paper too. The problem is the ordering of the statements, In my predicate, I check "n != null && n.Valid()" first. Since it was giving me an error, I didn't bother to write "n.footprint <= footprint" in the predicate.

Divyanshu Ranjan Over a year ago

Ah, probably order didn't mattered in earlier versions of dafny. It do now it seems

Collectives™ on Stack Overflow

Dafny linked queue implementation

1 Answer 1

2 Comments

Your Answer

Hot Network Questions

Collectives™ on Stack Overflow

1 Answer 1

2 Comments

Your Answer

Sign up or log in

Post as a guest

Related