Resource Usage Protocols for Iterators

By: Christian Haack, Clément Hurlin


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.

Cite as:

Christian Haack, Clément Hurlin, “Resource Usage Protocols for Iterators”, Journal of Object Technology, Volume 8, no. 4 (June 2009), pp. 55-83, doi:10.5381/jot.2009.8.4.a3.

PDF | HTML | DOI | BiBTeX | Tweet this | Post to CiteULike | Share on LinkedIn

The JOT Journal   |   ISSN 1660-1769   |   DOI 10.5381/jot   |   AITO   |   Open Access