TY - JOUR
T1 - Towards imperative modules
T2 - Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science
AU - Naumann, David A.
AU - Barnett, Mike
PY - 2004
Y1 - 2004
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 local co-dependence, 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.
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 local co-dependence, 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.
UR - http://www.scopus.com/inward/record.url?scp=4544323610&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=4544323610&partnerID=8YFLogxK
U2 - 10.1109/lics.2004.1319626
DO - 10.1109/lics.2004.1319626
M3 - Conference article
AN - SCOPUS:4544323610
SN - 1043-6871
VL - 19
SP - 313
EP - 322
JO - Proceedings - Symposium on Logic in Computer Science
JF - Proceedings - Symposium on Logic in Computer Science
Y2 - 13 July 2004 through 17 July 2004
ER -