Ownership confinement ensures representation independence for object-oriented programs

DOI10.1145/1101821.1101824MaRDI QIDQ3546287zbMATH OpenOpenAlexWikidataFDO

Authors Anindya Banerjee, David A. Naumann

Publication date 21 December 2008

Published in Journal of the ACM (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/cs/0212003

Mathematics Subject Classification ID

Theory of programming languages (68N15) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Abstract: Dedicated to the memory of Edsger W.Dijkstra. Representation independence or relational parametricity 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 paper 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 a restriction, 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.

Recommendations

• Ownership types for object encapsulation
• scientific article; zbMATH DE number 1728235
• Infering Ownership Types for Encapsulated Object-Oriented Program Components
• Dynamic Access Control in a Concurrent Object Calculus

Cited in

(28)

• Automating regression verification of pointer programs by predicate abstraction
• Towards patterns for heaps and imperative lambdas
• Confinement framework for encapsulating objects
• On assertion-based encapsulation for object invariants and simulations
• scientific article; zbMATH DE number 1728235 (Why is no real title available?)
• Laws of programming for references
• Ownership types for object encapsulation
• Synchronizing model and program refactoring
• Full abstraction at package boundaries of object-oriented languages
• Featherweight generic confinement
• A semantic model of confinement and locality theorem
• Infering Ownership Types for Encapsulated Object-Oriented Program Components
• scientific article; zbMATH DE number 1304000 (Why is no real title available?)
• Refactoring and representation independence for class hierarchies
• Verification of object-oriented programs: a transformational approach
• scientific article; zbMATH DE number 2079618 (Why is no real title available?)
• JAC—Access right based encapsulation for Java
• Category theoretic models of data refinement
• Holistic Specifications for Robust Programs
• Representation independence, confinement and access control (extended abstract)
• Protecting representation with effect encapsulation
• A Representation-Independent Behavioral Semantics for Object-Oriented Components
• Type-based confinement
• Observable interface behaviour and inheritance
• Formal Methods for Components and Objects
• Blaming the client: on data refinement in the presence of pointers
• Towards imperative modules: reasoning about invariants and sharing of mutable state
• Observational purity and encapsulation

This page was built for publication: Ownership confinement ensures representation independence for object-oriented programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3546287)