Formal specification and verification of Java refactorings

Alejandra Garrido, Jose Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

There is an extensive literature about refactorings of object-oriented programs, and many refactoring tools for the Java programming language. However, except for a few studies, in practice it is difficult to find precise formal specifications of the preconditions and mechanisms of automated refactorings. Moreover, there is usually no formal proof that a refactoring is correct, i.e., that it preserves the behavior of the program. We present an equational semantics based approach to Java refactoring. Specifically, we use an executable Java formal semantics in the Maude language to: (i) formally specify three useful Java refactorings; and (ii) give detailed proofs of correctness for two of those refactorings, showing that they are behavior-preserving transformations. Besides the obvious benefits of providing rigorous specifications for refactoring tool builders and rigorous correctness guarantees, our approach has the additional advantage of its executability: our formal refactoring specifications can be used directly to refactor Java programs and yield a provably correct Java refactoring tool.

Original languageEnglish (US)
Title of host publicationProceedings - Sixth IEEE International Workshop on Source Code Analysis and Manipulation, SCAM 2006
Pages165-174
Number of pages10
DOIs
StatePublished - Dec 1 2006
Event6th IEEE International Workshop on Source Code Analysis and Manipulation, SCAM 2006 - Philadelphia, PA, United States
Duration: Sep 27 2006Sep 29 2006

Publication series

NameProceedings - Sixth IEEE International Workshop on Source Code Analysis and Manipulation, SCAM 2006

Other

Other6th IEEE International Workshop on Source Code Analysis and Manipulation, SCAM 2006
CountryUnited States
CityPhiladelphia, PA
Period9/27/069/29/06

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Formal specification and verification of Java refactorings'. Together they form a unique fingerprint.

  • Cite this

    Garrido, A., & Meseguer, J. (2006). Formal specification and verification of Java refactorings. In Proceedings - Sixth IEEE International Workshop on Source Code Analysis and Manipulation, SCAM 2006 (pp. 165-174). [4026866] (Proceedings - Sixth IEEE International Workshop on Source Code Analysis and Manipulation, SCAM 2006). https://doi.org/10.1109/SCAM.2006.16