Trustworthy Refactoring via Decomposition and Schemes: A Complex Case Study
Abstract
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.
Cite
@article{arxiv.1708.07225,
title = {Trustworthy Refactoring via Decomposition and Schemes: A Complex Case Study},
author = {Dániel Horpácsi and Judit Kőszegi and Zoltán Horváth},
journal= {arXiv preprint arXiv:1708.07225},
year = {2017}
}
Comments
In Proceedings VPT 2017, arXiv:1708.06887