TY - JOUR
T1 - Ownership confinement ensures representation independence for object-oriented programs
AU - Banerjee, Anindya
AU - Naumann, David A.
PY - 2005
Y1 - 2005
N2 - Representation independence formally characterizes the encapsulation provided by language constructs for data abstraction and justifies reasoning by simulation. Representation independence has been shown for a variety of languages and constructs but not for shared references to mutable state; indeed it fails in general for such languages. This article formulates representation independence for classes, in an imperative, object-oriented language with pointers, subclassing and dynamic dispatch, class oriented visibility control, recursive types and methods, and a simple form of module. An instance of a class is considered to implement an abstraction using private fields and so-called representation objects. Encapsulation of representation objects is expressed by arestriction, called confinement, on aliasing. Representation independence is proved for programs satisfying the confinement condition. A static analysis is given for confinement that accepts common designs such as the observer and factory patterns. The formalization takes into account not only the usual interface between a client and a class that provides an abstraction but also the interface (often called "protected") between the class and its subclasses.
AB - Representation independence formally characterizes the encapsulation provided by language constructs for data abstraction and justifies reasoning by simulation. Representation independence has been shown for a variety of languages and constructs but not for shared references to mutable state; indeed it fails in general for such languages. This article formulates representation independence for classes, in an imperative, object-oriented language with pointers, subclassing and dynamic dispatch, class oriented visibility control, recursive types and methods, and a simple form of module. An instance of a class is considered to implement an abstraction using private fields and so-called representation objects. Encapsulation of representation objects is expressed by arestriction, called confinement, on aliasing. Representation independence is proved for programs satisfying the confinement condition. A static analysis is given for confinement that accepts common designs such as the observer and factory patterns. The formalization takes into account not only the usual interface between a client and a class that provides an abstraction but also the interface (often called "protected") between the class and its subclasses.
KW - Alias control
KW - Confinement
KW - Data refinement
KW - Relational parametricity
KW - Simulation
UR - http://www.scopus.com/inward/record.url?scp=33745220946&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=33745220946&partnerID=8YFLogxK
U2 - 10.1145/1101821.1101824
DO - 10.1145/1101821.1101824
M3 - Article
AN - SCOPUS:33745220946
SN - 0004-5411
VL - 52
SP - 894
EP - 960
JO - Journal of the ACM (JACM)
JF - Journal of the ACM (JACM)
IS - 6
ER -