TY - JOUR
T1 - Towards imperative modules
T2 - Reasoning about invariants and sharing of mutable state
AU - Naumann, David A.
AU - Barnett, Mike
PY - 2006/11/10
Y1 - 2006/11/10
N2 - Imperative and object-oriented programs make ubiquitous use of shared mutable objects. Updating a shared object can and often does transgress a boundary that was supposed to be established using static constructs such as a class with private fields. This paper shows how auxiliary fields can be used to express two state-dependent encapsulation disciplines: ownership, a kind of separation, and friendship, a kind of sharing. A methodology is given for specification and modular verification of encapsulated object invariants and shown sound for a class-based language. As an example the methodology is used to specify iterators, which are problematic for previous ownership systems.
AB - Imperative and object-oriented programs make ubiquitous use of shared mutable objects. Updating a shared object can and often does transgress a boundary that was supposed to be established using static constructs such as a class with private fields. This paper shows how auxiliary fields can be used to express two state-dependent encapsulation disciplines: ownership, a kind of separation, and friendship, a kind of sharing. A methodology is given for specification and modular verification of encapsulated object invariants and shown sound for a class-based language. As an example the methodology is used to specify iterators, which are problematic for previous ownership systems.
KW - Alias control
KW - Data abstraction
KW - Object invariants
KW - Program verification
UR - http://www.scopus.com/inward/record.url?scp=33750236160&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=33750236160&partnerID=8YFLogxK
U2 - 10.1016/j.tcs.2006.07.035
DO - 10.1016/j.tcs.2006.07.035
M3 - Article
AN - SCOPUS:33750236160
SN - 0304-3975
VL - 365
SP - 143
EP - 168
JO - Theoretical Computer Science
JF - Theoretical Computer Science
IS - 1-2
ER -