Previous article

Next article

Resource Usage Protocols for Iterators

Christian Haack, Radboud University Nijmegen, The Netherlands
Clément Hurlin, University of Twente, The Netherlands, and INRIA Sophia-Antipolis, France


PDF Icon
PDF Version


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.

Note: Due to the typographical sophistication of this article, no HTML version is available. Please use the PDF version.

About the authors

Christian Haack ( was a researcher in the Digital Security Group at Radboud University Nijmegen in The Netherlands, while doing this research. He now works for aicas realtime — a company that develops Realtime Java technology — in Karlsruhe, Germany. He remains in close touch with Radboud University and has a web page at˜chaack.

Clément Hurlin ( is a PhD student in the Everest team at Inria Sophia-Antipolis in France. He is currently visiting the Formal Methods & Tools group at University of Twente in The Netherlands. He has a web page at

Christian Haack, Clément Hurlin: "Resource Usage Protocols for Iterators", in Journal of Object Technology, vol. 8, no. 4, Special Issue: Workhop FTfJP and IWACO at ECOOP 08, June 2009, pp. 55-83

Previous article

Next article