CODEWITHSUNDEEP
dafny
Daniel Ricketts
Daniel Ricketts

Reputation: 447

Dafny iterator: precondition and modifes clause violated

Dafny shows multiple errors when calling MoveNext() on an iterator that does nothing:

iterator Iter()
{}

method main()
    decreases *
{
    var iter := new Iter();
    while (true)
        decreases *
    {
        var more := iter.MoveNext();
        if (!more) { break; }
    }
}

The errors are on the call to iter.MoveNext():

call may violate context's modifies clause

A precondition for this call might not hold.

There is no modifies clause for main or Iter, and there is no precondition for Iter. Why is this program incorrect?

Upvotes: 1

Views: 71

Answers (1)

James Wilcox
James Wilcox

Reputation: 5663

You need the following invariant on the loop

invariant iter.Valid() && fresh(iter._new)

Then your program verifies. As usual, there's nothing wrong (dynamically) with your program, but you can have false positives at verification time due to missing annotations.

As far as I know, this invariant is always required when using iterators.

(A little) More information about iterators can be found in the Dafny Reference, in Chapter 16. (At least, enough information for me to remember the answer to this question.)

Upvotes: 1

Related Questions