Trustworthy Refactoring via Decomposition and Schemes: A Complex Case Study

Dániel Horpácsi
Judit Kőszegi
Zoltán Horváth

Widely used complex code refactoring tools lack a solid reasoning about the correctness of the transformations they implement, whilst interest in proven correct refactoring is ever increasing as only formal verification can provide true confidence in applying tool-automated refactoring to industrial-scale code. By using our strategic rewriting based refactoring specification language, we present the decomposition of a complex transformation into smaller steps that can be expressed as instances of refactoring schemes, then we demonstrate the semi-automatic formal verification of the components based on a theoretical understanding of the semantics of the programming language. The extensible and verifiable refactoring definitions can be executed in our interpreter built on top of a static analyser framework.

In Alexei Lisitsa, Andrei P. Nemytykh and Maurizio Proietti: Proceedings Fifth International Workshop on Verification and Program Transformation (VPT 2017), Uppsala, Sweden, 29th April 2017, Electronic Proceedings in Theoretical Computer Science 253, pp. 92–108.
Published: 23rd August 2017.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: