Support for Iterators

[wadoon]

This issue was created at git.key-project.org where the discussions are preserved.

---

Overview

Verifying programs that use iterators in KeY is currently very difficult. There are neither taclets for dealing with iterators nor contracts for hasNext() and next().

Specific Problems

How to specify the iterator interface

What would a specification for Iterator look like?

This depends to a large part on the prevalent use cases of iterators in actual programs. Are there are many instance of custom subclasses of Iterator or do most programs just use the iterators from the Standard Library? Are iterators mostly used in a straightforward or in a more complex (iterating over multiple collections at once, having multiple iterators over the same collection, modifying the collection while it is being iterated over) way?

One problem that makes working with iterators difficult is that next() cannot be implemented as a pure method, but it is not clear what it should modify. Some possibilities include:

1. An index for the sequence to be iterated over
2. A sequence containing all elements that have been iterated over
3. A sequence containing all elements still to be iterated over

All of these require either a model or ghost field for a sequence. What does this sequence depend on? Depending on the prevalent use cases, one may simply disallow modifying the collection being iterated over in the loop. In that case, the sequence would be determined by the elements that are in the collection at the time the iterator is created, and by the order in which the collection will be iterated over, which needs to be specified somehow as well. Otherwise, things become more complicated as the sequence may change in between calls to next(). The sequence thus also depends on the way the collection is modified during the loop.

Implicit assignable clause for loop invariants & loop contracts

Observe the following program:

Iterator it = list.iterator();

//@ assignable it.*;
while (it.hasNext()) {
    do something with it.next()
}

If we convert this while loop into an enhanced for loop (for(Object element : list)), the assignable clause can no longer be expressed because we don't have a variable named it.

The solution to this depends largely on the solution for the previous problem. One possible solution may be to introduce a new keyword for this variable (like \index and \values). Another, more user-friendly, solution may be to modify the assignable clause implicitly. Specifically, we would need to add the assignable set of next() to that of the loop.

---

Information:

• created_at: 2019-04-02T14:23:45.811Z
• updated_at: 2019-04-02T14:26:27.702Z
• closed_at: None (closed_by: )
• milestone:
• user_notes_count: 0