CODEWITHSUNDEEP
dafny
Daniel Ricketts
Daniel Ricketts

Reputation: 447

Dafny can't verify multiple iterators in while loop

I want to have a function that allocates two iterators, and then goes into a loop that repeatedly calls MoveNext() on the iterators for as long as MoveNext() returns true. However, calling MoveNext() on what iterator violates (or prevents Dafny from verifying) the invariant necessary for the other iterator:

iterator Iter1()
{ yield; }

iterator Iter2()
{ yield; }

method main()
    decreases *
{
    var iter1 := new Iter1();
    var iter2 := new Iter2();
    var iter1More := true;
    var iter2More := true;

    while (iter1More || iter2More)
        invariant iter1More ==> iter1.Valid() && fresh(iter1._new)
        // The following invariant is not verified
        invariant iter2More ==> iter2.Valid() && fresh(iter2._new)
        decreases *
    {
        if (iter1More) {
            iter1More := iter1.MoveNext();
        }
    }
}

Dafny cannot verify iter2More ==> iter2.Valid() && fresh(iter2._new), even though Iter1 has an empty modifies clause. Is there a loop invariant I need to add?

Upvotes: 1

Views: 229

Answers (1)

James Wilcox
James Wilcox

Reputation: 5663

Okay, this one was fun :)

Here's the additional invariant you need to verify it

invariant {iter1} + iter1._new !! {iter2} + iter2._new

This invariant is also sufficient to prove a more complex loop that calls both iterators, like this:

    if (iterMore1) {
        iterMore1 := iter1.MoveNext();
    }
    if (iterMore2) {
        iterMore2 := iter2.MoveNext();
    }

The way I figured this out was that Dafny was complaining that iter2.Valid() might not hold after the call to iter1.MoveNext(). Any time a predicate that was true before a call might not be true after the call, you know the problem is that Dafny could not prove the reads clause of the function did not overlap with the modifies clause of the method. Unfortunately, neither the reads clause of an iterator's Valid() predicate, nor the modifies clause of an iterator's MoveNext() method are documented. I dove into the Boogie output of Dafny and was able to reverse engineer them as follows

predicate Valid()
  reads this, this._reads, this._new

method MoveNext()
  modifies this, this._modifies, old(this._new)

I was also able to see that Dafny can show that both Iter1 and Iter2 have empty _reads and _modifies sets. So really it's just the references themselves, and their _new sets. This explains the invariant.

Upvotes: 1

Related Questions