CODEWITHSUNDEEP
dafny
Daniel Ricketts
Daniel Ricketts

Reputation: 447

Dafny iterator on heap fails to ensure Valid()

I have a class that allocates an iterator on the heap and calls MoveNext() on that iterator. I want to prove that if MoveNext() returns true, Valid() holds for the iterator.

iterator Iter()
{}

class MyClass
{
    var iter : Iter;

    constructor ()
    {
        iter := new Iter();
    }
    method next() returns (more : bool)
    requires iter.Valid();
    modifies iter, iter._new, iter._modifies;
    {
        more := iter.MoveNext();
        // This assertion fails:
        assert more ==> iter.Valid();
    }
}

I took a look at the output of /rprint, and the method MoveNext() contains ensures more ==> this.Valid(), which seems to imply my desired assertion. If I change iter to be locally allocated within the method next(), then Dafny verifies the assertion.

Upvotes: 0

Views: 86

Answers (1)

Rustan Leino
Rustan Leino

Reputation: 2097

The problem is that nothing is known about what's in iter._new and iter._modifies. If this is in one of those sets, then this.iter may have changed during the call to MoveNext().

This body for next() confirms what I just said:

var i := iter;
more := iter.MoveNext();
assert i == iter;  // this assertion fails
assert more ==> iter.Valid();

So, under the assumption more, Valid() does still hold of the iterator, but the iterator may no longer referenced by iter:

more := iter.MoveNext();
assert more ==> old(iter).Valid();  // this holds

Probably the way you want to solve this problem is to add a precondition to next():

method next() returns (more : bool)
  requires iter.Valid()
  requires this !in iter._new + iter._modifies  // add this precondition
  modifies iter, iter._new, iter._modifies
{
  more := iter.MoveNext();
  assert more ==> iter.Valid();  // this now verifies
}

Rustan

Upvotes: 1

Related Questions