1CS - Computing Science Department (Radboud University of Nijmegen Faculty of Science Institute for Computing and Information Sciences Postbus 9010 6500 GL Nijmegen - Pays-Bas)
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.
Type de document :
Article dans une revue
The Journal of Object Technology, Chair of Software Engineering, 2009, Special Issue Workshops IWACO and FTFJP at ECOOP 08, 8 (4), pp.55-83
https://hal.inria.fr/inria-00410128
Contributeur : Clément Hurlin
<>
Soumis le : lundi 17 août 2009 - 19:15:27
Dernière modification le : samedi 27 janvier 2018 - 01:31:26
Christian Haack, Clément Hurlin. Resource usage protocols for iterators. The Journal of Object Technology, Chair of Software Engineering, 2009, Special Issue Workshops IWACO and FTFJP at ECOOP 08, 8 (4), pp.55-83. 〈inria-00410128〉
