State based encapsulation for modular reasoning about behavior-preserving refactorings

Anindya Banerjee, David A. Naumann

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review

4 Scopus citations

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 chapter 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.

Original languageEnglish
Title of host publicationAliasing in Object-Oriented Programming
Subtitle of host publicationTypes, Analysis, and Verification
Pages319-365
Number of pages47
DOIs
StatePublished - 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7850
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Dive into the research topics of 'State based encapsulation for modular reasoning about behavior-preserving refactorings'. Together they form a unique fingerprint.

Cite this