Resource Usage Protocols for Iterators.
Christian Haack, Clément Hurlin · The Journal of Object Technology · 2009
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. This is an extended version of a paper at the International Workshop on Aliasing, Ownership and Confinement (IWACO 2008).1 Supported in part by IST-FET-2005-015905 Mobius project.2 Supported in part by