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

(27)

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

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)