Resource Usage Protocols for Iterators
We discuss usage protocols for iterator objects that prevent concurrent
modifications of the underlying collection while iterators are in progress.
We formalize these protocols in Java-like object interfaces, enriched with
separation logic contracts. We present examples of iterator clients and
proofs that they adhere to the iterator protocol, as well as examples
of iterator implementations and proofs that they implement the iterator
interface.