Ownership confinement ensures representation independence for object-oriented programs

Anindya Banerjee, David A. Naumann

Research output: Contribution to journalArticlepeer-review

62 Scopus citations

Abstract

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.

Original languageEnglish
Pages (from-to)894-960
Number of pages67
JournalJournal of the ACM (JACM)
Volume52
Issue number6
DOIs
StatePublished - 2005

Keywords

  • Alias control
  • Confinement
  • Data refinement
  • Relational parametricity
  • Simulation

Fingerprint

Dive into the research topics of 'Ownership confinement ensures representation independence for object-oriented programs'. Together they form a unique fingerprint.

Cite this