State Based Ownership, Reentrance, and Encapsulation

Abstract. A properly encapsulated data representation can be revised for refactoring or other purposes without affecting the correctness of client programs and extensions of a class. But encapsulation is difficult to achieve in object-oriented programs owing to heap based structures and reentrant callbacks. This paper shows that it is achieved by a discipline using assertions and auxiliary fields to manage invariants and transferrable ownership. The main result is representation independence: a rule for modular proof of equivalence of class implementations.

• Type: Conference
• Year: 2005
• Where: ECOOP
• Authors: Anindya Banerjee, David A. Naumann
• Keywords: Client Programs, Data Representation, ECOOP 2005, Object-oriented Programs, Programming Languages