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 |
 |
REFEREED
ARTICLE
PDF Version |
Abstract
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 (chaack@cs.ru.nl) 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 http://www.cs.ru.nl/˜chaack.
|
Clément Hurlin (clement.hurlin@sophia.inria.fr) 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 http://wwwsop.inria.fr/everest/personnel/Clement.Hurlin. |
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 http://www.jot.fm/issues/issue_2009_06/article3/
|