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

research-article

Challenge proposal: verification of refactorings

Authors:

Torbjörn Ekman,

Oege de MoorAuthors Info & Claims

PLPV '09: Proceedings of the 3rd workshop on Programming languages meets program verification

Pages 67 - 72

https://doi.org/10.1145/1481848.1481859

Published: 20 January 2009 Publication History

Abstract

Automated refactoring tools are an essential part of a software developer's toolbox. They are most useful for gradually improving large existing code bases and it is essential that they work reliably, since even a simple refactoring may affect many different parts of a program, and the programmer should not have to inspect every individual change to ensure that the transformation went as expected. Even extensively tested industrial-strength refactoring engines, however, are fraught with many bugs that lead to incorrect, non-behaviour preserving transformations. We argue that software refactoring tools are a prime candidate for mechanical verification, offering significant challenges but also the prospect of tangible benefits for real-world software development.

References

[1]

Gavin M. Bierman, Matthew J. Parkinson, and Andrew M. Pitts. MJ: An imperative core calculus for Java and Java with effects. Technical Report 563, University of Cambridge, 2003.

[2]

Sandrine Blazy, Zaynah Dargaye, and Xavier Leroy. Formal verification of a C compiler front-end. In FM 2006: International Symposium on Formal Methods, volume 4085 of LNCS, pages 460--475. Springer, 2006.

Digital Library

[3]

Torbjörn Ekman, Ran Ettinger, Max Schäfer, and Mathieu Verbaere. Refactoring bugs, 2008. http://progtools.comlab.ox.ac.uk/refactoring/bugreports.

[4]

Torbjörn Ekman and Görel Hedin. The JastAdd Extensible Java Compiler. In OOPSLA, 2007.

Digital Library

[5]

Torbjörn Ekman, Max Schäfer, and Mathieu Verbaere. Refactoring is not (yet) about transformation. In Second Workshop on Refactoring Tools (WRT), 2008.

Digital Library

[6]

H.-Christian Estler, Thomas Ruhroth, and Heike Wehrheim. Modelchecking Correctness of Refactorings -- Some Experiments. Electronic Notes in Theoretical Computer Science, 187:3--17, 2007.

Digital Library

[7]

Rodney Farrow. Automatic generation of fixed-point-finding evaluators for circular, but well-defined, attribute grammars. In CC, pages 85--98, 1986.

Digital Library

[8]

Alejandra Garrido and José Meseguer. Formal Specification and Verification of Java Refactorings. In SCAM, 2006.

Digital Library

[9]

James Gosling, Bill Joy, Guy Steele, and Gilad Bracha. The Java Language Specification. 2005.

Digital Library

[10]

Görel Hedin. Reference Attributed Grammars. Informatica, (24):301--317, 2000.

[11]

Gérard P. Huet. The Zipper. J. Funct. Program., 7(5):549--554, 1997.

Digital Library

[12]

Atsushi Igarashi and Benjamin C. Pierce. On inner classes. Inf. and Comp., 177(1):56--89, 2002.

Digital Library

[13]

Gerwin Klein and Tobias Nipkow. A machine-checked model for a Java-like language, virtual machine, and compiler. ACM Trans. Program. Lang. Syst., 28(4):619--695, 2006.

Digital Library

[14]

Günter Kniesel and Helge Koch. Static composition of refactorings. Science of Computer Programming, 52(1-3):9--51, 2004.

Digital Library

[15]

Donald E. Knuth. Semantics of context-free languages. Mathematical Systems Theory, 2:127--146, 1968. Correction: Mathematical Systems Theory, 5:95--96, 1971.

[16]

Sorin Lerner, Todd Millstein, Erika Rice, and Craig Chambers. Automated soundness proofs for dataflow analyses and transformations via local rules. SIGPLAN Not., 40(1):364--377, 2005.

Digital Library

[17]

Xavier Leroy. Formal certification of a compiler back-end. In POPL, pages 42--54, 2006.

Digital Library

[18]

Eva Magnusson and Görel Hedin. Circular Reference Attributed Grammars. Sci. Comput. Program., 68(1):21--37, 2007.

Digital Library

[19]

The Maude System. http://maude.cs.uiuc.edu.

[20]

Max Schäfer, Torbjörn Ekman, and Oege de Moor. Formalising and Verifying Reference Attribute Grammars in Coq (Technical Report). http://progtools.comlab.ox.ac.uk/projects/refactoring/formalising-rags, 2008.

[21]

Max Schäfer, Torbjörn Ekman, and Oege de Moor. Sound and Extensible Renaming for Java. In Gregor Kiczales, editor, OOPSLA. ACM Press, 2008.

Digital Library

[22]

Generic Programming with Strafunski. http://www.cs.vu.nl/Strafunski.

[23]

Stratego/XT. http://www.program-transformation. org/Stratego.

[24]

Nik Sultana and Simon Thompson. Mechanical Verification of Refactorings. In PEPM. ACM SIGPLAN, January 2008.

Digital Library

[25]

Mathieu Verbaere. A Language to Script Refactoring Transformations. D.Phil. thesis, Oxford University Computing Laboratory, 2008.

[26]

Philip Wadler. The Expression Problem. Message to Java-genericity mailing list, 1998.

Cited By

Oliveira JGheyi RPontes FMongiovi MRibeiro MGarcia A(2020)Revisiting Refactoring Mechanics from Tool Developers’ PerspectiveFormal Methods: Foundations and Applications10.1007/978-3-030-63882-5_3(25-42)Online publication date: 19-Nov-2020
https://doi.org/10.1007/978-3-030-63882-5_3
Wang KZhu CCelik AKim JBatory DGligoric MChaudron MCrnkovic IChechik MHarman M(2018)Towards refactoring-aware regression test selectionProceedings of the 40th International Conference on Software Engineering10.1145/3180155.3180254(233-244)Online publication date: 27-May-2018
https://dl.acm.org/doi/10.1145/3180155.3180254
Mongiovi MGheyi RSoares GRibeiro MBorba PTeixeira L(2018)Detecting Overly Strong Preconditions in Refactoring EnginesIEEE Transactions on Software Engineering10.1109/TSE.2017.269398244:5(429-452)Online publication date: 1-May-2018
https://doi.org/10.1109/TSE.2017.2693982
Show More Cited By

Index Terms

Challenge proposal: verification of refactorings
1. Software and its engineering
  1. Software notations and tools
    1. Compilers

Recommendations

Tool-Supported Refactoring of Existing Object-Oriented Code into Aspects

Aspect-Oriented Programming (AOP) provides mechanisms for the separation of crosscutting concerns—functionalities scattered through the system and tangled with the base code. Existing systems are a natural testbed for the AOP approach since they often ...
Towards an appropriate software refactoring tool support
ACS'09: Proceedings of the 9th WSEAS international conference on Applied computer science

Refactoring is a technique that is concerned with changing internal software design while external software behaviour is preserved. Although the refactoring process seems to be clear and well defined, there are difficulties with regard to its ...
Are monitoring crosscutting concerns really refactorable into aspects?: an empirical study
IWOR '19: Proceedings of the 3rd International Workshop on Refactoring

Monitoring concerns' implementation crosscuts a software's system core concerns' implementation, leading to difficult to maintain and understand source code. Other paradigms have been proposed for crosscutting concerns implementation that should improve ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLPV '09: Proceedings of the 3rd workshop on Programming languages meets program verification

January 2009

90 pages

ISBN:9781605583303

DOI:10.1145/1481848

Program Chairs:
Thorsten Altenkirch
University of Nottingham, UK
,
Todd Millstein
University of California, Los Angeles, USA

Copyright © 2009 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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 20 January 2009

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL09

Sponsor:

POPL09: The 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 20, 2009

GA, Savannah, USA

Acceptance Rates

Overall Acceptance Rate 18 of 25 submissions, 72%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
329
Total Downloads

Downloads (Last 12 months)5
Downloads (Last 6 weeks)1

Reflects downloads up to 09 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Oliveira JGheyi RPontes FMongiovi MRibeiro MGarcia A(2020)Revisiting Refactoring Mechanics from Tool Developers’ PerspectiveFormal Methods: Foundations and Applications10.1007/978-3-030-63882-5_3(25-42)Online publication date: 19-Nov-2020
https://doi.org/10.1007/978-3-030-63882-5_3
Wang KZhu CCelik AKim JBatory DGligoric MChaudron MCrnkovic IChechik MHarman M(2018)Towards refactoring-aware regression test selectionProceedings of the 40th International Conference on Software Engineering10.1145/3180155.3180254(233-244)Online publication date: 27-May-2018
https://dl.acm.org/doi/10.1145/3180155.3180254
Mongiovi MGheyi RSoares GRibeiro MBorba PTeixeira L(2018)Detecting Overly Strong Preconditions in Refactoring EnginesIEEE Transactions on Software Engineering10.1109/TSE.2017.269398244:5(429-452)Online publication date: 1-May-2018
https://doi.org/10.1109/TSE.2017.2693982
Medeiros FRibeiro MGheyi RApel SKastner CFerreira BCarvalho LFonseca B(2018)Discipline Matters: Refactoring of Preprocessor Directives in the #ifdef HellIEEE Transactions on Software Engineering10.1109/TSE.2017.268833344:5(453-469)Online publication date: 1-May-2018
https://doi.org/10.1109/TSE.2017.2688333
Cohen J(2016)Renaming Global Variables in C Mechanically Proved CorrectElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.216.3216(50-64)Online publication date: 6-Jul-2016
https://doi.org/10.4204/EPTCS.216.3
Visser EWachsmuth GTolmach ANeron PVergu VPassalaqua AKonat GBlack AKrishnamurthi SBruegge BRuskiewicz J(2014)A Language Designer's WorkbenchProceedings of the 2014 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software10.1145/2661136.2661149(95-111)Online publication date: 20-Oct-2014
https://dl.acm.org/doi/10.1145/2661136.2661149
Mongiovi MMendes GGheyi RSoares GRibeiro M(2014)Scaling Testing of Refactoring EnginesProceedings of the 2014 IEEE International Conference on Software Maintenance and Evolution10.1109/ICSME.2014.59(371-380)Online publication date: 29-Sep-2014
https://dl.acm.org/doi/10.1109/ICSME.2014.59
Soares GGheyi RMurphy-Hill EJohnson B(2013)Comparing approaches to analyze refactoring activity on software repositoriesJournal of Systems and Software10.1016/j.jss.2012.10.04086:4(1006-1022)Online publication date: 1-Apr-2013
https://dl.acm.org/doi/10.1016/j.jss.2012.10.040
Soares GLeavens G(2012)Automated behavioral testing of refactoring enginesProceedings of the 3rd annual conference on Systems, programming, and applications: software for humanity10.1145/2384716.2384760(105-106)Online publication date: 19-Oct-2012
https://dl.acm.org/doi/10.1145/2384716.2384760
Soares GLeavens G(2012)Automated behavioral testing of refactoring enginesProceedings of the 3rd annual conference on Systems, programming, and applications: software for humanity10.1145/2384716.2384737(49-52)Online publication date: 19-Oct-2012
https://dl.acm.org/doi/10.1145/2384716.2384737
Show More Cited By

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