State based encapsulation for modular reasoning about behavior-preserving refactorings

Anindya Banerjee; David A. Naumann

doi:10.1007/978-3-642-36946-9_12

State based encapsulation for modular reasoning about behavior-preserving refactorings

Anindya Banerjee
, David A. Naumann

Department of Computer Science

IMDEA Software Institute

Research output: Chapter in Book/Report/Conference proceeding › Chapter › peer-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 language	English
Title of host publication	Aliasing in Object-Oriented Programming
Subtitle of host publication	Types, Analysis, and Verification
Pages	319-365
Number of pages	47
DOIs	https://doi.org/10.1007/978-3-642-36946-9_12
State	Published - 2013

Publication series

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

Access to Document

10.1007/978-3-642-36946-9_12

Cite this

Banerjee, A., & Naumann, D. A. (2013). State based encapsulation for modular reasoning about behavior-preserving refactorings. In Aliasing in Object-Oriented Programming: Types, Analysis, and Verification (pp. 319-365). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7850). https://doi.org/10.1007/978-3-642-36946-9_12

@inbook{8b7e6217caad4537b935ebf0fc46f076,

title = "State based encapsulation for modular reasoning about behavior-preserving refactorings",

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.",

author = "Anindya Banerjee and Naumann, \{David A.\}",

year = "2013",

doi = "10.1007/978-3-642-36946-9\_12",

language = "English",

isbn = "9783642369452",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "319--365",

booktitle = "Aliasing in Object-Oriented Programming",

}

Banerjee, A & Naumann, DA 2013, State based encapsulation for modular reasoning about behavior-preserving refactorings. in Aliasing in Object-Oriented Programming: Types, Analysis, and Verification. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7850, pp. 319-365. https://doi.org/10.1007/978-3-642-36946-9_12

State based encapsulation for modular reasoning about behavior-preserving refactorings. / Banerjee, Anindya; Naumann, David A.
Aliasing in Object-Oriented Programming: Types, Analysis, and Verification. 2013. p. 319-365 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7850).

Research output: Chapter in Book/Report/Conference proceeding › Chapter › peer-review

TY - CHAP

T1 - State based encapsulation for modular reasoning about behavior-preserving refactorings

AU - Banerjee, Anindya

AU - Naumann, David A.

PY - 2013

Y1 - 2013

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

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

UR - https://www.scopus.com/pages/publications/84875978886

UR - https://www.scopus.com/pages/publications/84875978886#tab=citedBy

U2 - 10.1007/978-3-642-36946-9_12

DO - 10.1007/978-3-642-36946-9_12

M3 - Chapter

AN - SCOPUS:84875978886

SN - 9783642369452

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 319

EP - 365

BT - Aliasing in Object-Oriented Programming

ER -

Banerjee A, Naumann DA. State based encapsulation for modular reasoning about behavior-preserving refactorings. In Aliasing in Object-Oriented Programming: Types, Analysis, and Verification. 2013. p. 319-365. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-36946-9_12

State based encapsulation for modular reasoning about behavior-preserving refactorings

Abstract

Publication series

Access to Document

Other files and links

Fingerprint

Cite this