More Web Proxy on the site http://driver.im/

extended-abstract

Refactoring and representation independence for class hierarchies: extended abstract

Authors:

David A. Naumann,

Augusto SampaioAuthors Info & Claims

FTFJP '10: Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs

Article No.: 8, Pages 1 - 7

https://doi.org/10.1145/1924520.1924528

Published: 22 June 2010 Publication History

Abstract

Refactoring transformations are important for productivity and quality in software evolution. Modular reasoning about semantics preserving transformations is difficult even in typed class-based languages because transformations can change the internal representations for multiple interdependent classes and because encapsulation can be violated by pointers to mutable objects. In this paper, an existing theory of representation independence for a single class, based on a simple notion of ownership confinement, is generalized to a hierarchy of classes and used to prove several refactoring laws. Soundness of these laws was an open problem in an ongoing project on formal refactoring tools. The utility of the laws is shown in a case study. Shortcomings of the theory are described as a challenge to other approaches to heap encapsulation and relational reasoning for classes.

References

[1]

A. Ahmed, D. Dreyer, and A. Rossberg. State-dependent representation independence. In POPL, pages 340--353, 2009.

Digital Library

[2]

A. Banerjee and D. A. Naumann. Ownership confinement ensures representation independence for object-oriented programs. J. ACM, 52(6), 2005.

Digital Library

[3]

A. Banerjee and D. A. Naumann. State based ownership, reentrance, and encapsulation. In ECOOP, volume 3586 of LNCS, pages 387--411, 2005.

Digital Library

[4]

G. Bierman and M. Parkinson. Separation logic and abstraction. In POPL, pages 247--258, 2005.

Digital Library

[5]

L. Birkedal and H. Yang. Relational parametricity and separation logic. Logical Methods in Comp. Sci., 4(2), 2008.

[6]

P. Borba, A. Sampaio, A. Cavalcanti, and M. Cornélio. Algebraic reasoning for object-oriented programming. Sci. Comput. Programming, 52(1--3):53--100, 2004.

Digital Library

[7]

A. L. C. Cavalcanti and D. Naumann. A weakest precondition semantics for refinement of object-oriented programs. IEEE Trans. Softw. Eng., 26(8):713--728, 2000.

Digital Library

[8]

A. L. C. Cavalcanti and D. A. Naumann. Forward simulation for data refinement of classes. In Formal Methods Europe, volume 2391 of LNCS, pages 471--490, 2002.

Digital Library

[9]

D. Clarke and S. Drossopoulou. Ownership, encapsulation and the disjointness of type and effect. In OOPSLA, pages 292--310, Nov. 2002.

Digital Library

[10]

D. Dreyer, G. Neis, A. Rossberg, and L. Birkedal. A relational modal logic for higher-order stateful ADTs. In POPL, pages 185--198, 2010.

Digital Library

[11]

I. Filipović, P. O'Hearn, N. Torp-smith, and H. Yang. Blaming the client: On data refinement in the presence of pointers. Formal Aspects Comp., 2010.

[12]

V. Koutavas and M. Wand. Bisimulations for untyped imperative objects. In ESOP, volume 3924 of LNCS, pages 146--161, 2006.

Digital Library

[13]

V. Koutavas and M. Wand. Reasoning about class behavior. Informal proc. of FOOL/WOOD, 2007.

[14]

G. T. Leavens, D. A. Naumann, and S. Rosenberg. Preliminary definition of core JML. Technical Report CS Report 2006--07, Stevens Inst. Tech., 2006.

[15]

K. R. M. Leino and P. Müller. Object invariants in dynamic contexts. In ECOOP, pages 491--516, 2004.

[16]

P. Müller and A. Rudich. Ownership transfer in Universe Types. In OOPSLA, pages 461--478, 2007.

Digital Library

[17]

L. Silva, D. A. Naumann, and A. Sampaio. Refactoring and representation independence for class hierarchies. Draft journal paper, www.cs.stevens.edu/~naumann/pub/clHieDraft.pdf.

Digital Library

[18]

L. Silva, A. Sampaio, and Z. Liu. Laws of object-orientation with reference semantics. In SEFM, pages 217--226, 2008.

Digital Library

[19]

J. Smans, B. Jacobs, and F. Piessens. Implicit dynamic frames: Combining dynamic frames and separation logic. In ECOOP, pages 148--172, 2009.

Digital Library

[20]

E. Sumii. A complete characterization of observational equivalence in polymorphic lambda-calculus with general references. In Computer Science Logic, volume 5771 of LNCS, pages 455--469, 2009.

Digital Library

[21]

E. Sumii and B. C. Pierce. A bisimulation for type abstraction and recursion. J. ACM, 54(5), 2007.

Digital Library

Cited By

Welsch YPoetzsch-Heffter A(2011)Full abstraction at package boundaries of object-oriented languagesProceedings of the 14th Brazilian conference on Formal Methods: foundations and Applications10.1007/978-3-642-25032-3_3(28-43)Online publication date: 26-Sep-2011
https://dl.acm.org/doi/10.1007/978-3-642-25032-3_3

Index Terms

Refactoring and representation independence for class hierarchies: extended abstract
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Classes and objects
      2. Language types
        Object oriented languages

Recommendations

Refactoring and representation independence for class hierarchies

Refactoring transformations are important for productivity and quality in software evolution. Modular reasoning about semantics preserving transformations is difficult even in typed class-based languages because transformations can change the internal ...
Refactoring class hierarchies with KABA
OOPSLA '04

KABA is an innovative system for refactoring Java class hierar-chies. It uses the Snelting/Tip algorithm [13] in order to determine a behavior-preserving refactoring which is optimal with respect to a given set of client programs. KABA can be based on ...
State-dependent representation independence
POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Mitchell's notion of representation independence is a particularly useful application of Reynolds' relational parametricity -- two different implementations of an abstract data type can be shown contextually equivalent so long as there exists a relation ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

FTFJP '10: Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs

June 2010

66 pages

ISBN:9781450305402

DOI:10.1145/1924520

Copyright © 2010 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

CEKTRA
University of Maribor
AITO: Assoc Internationale por les Technologies Objects

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 22 June 2010

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Extended-abstract

Funding Sources

Conselho Nacional de Desenvolvimento Científico e Tecnológico
Division of Computing and Communication Foundations
National Institute of Science and Technology for Software Engineering (INES), funded by CNPq
Division of Computer and Network Systems

Conference

ECOOP '10

Sponsor:

AITO

ECOOP '10: European Conference on Object-Oriented Programming

June 22, 2010

Maribor, Slovenia

Acceptance Rates

Overall Acceptance Rate 51 of 75 submissions, 68%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
88
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 07 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Welsch YPoetzsch-Heffter A(2011)Full abstraction at package boundaries of object-oriented languagesProceedings of the 14th Brazilian conference on Formal Methods: foundations and Applications10.1007/978-3-642-25032-3_3(28-43)Online publication date: 26-Sep-2011
https://dl.acm.org/doi/10.1007/978-3-642-25032-3_3

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents