Trustworthy Refactoring via Decomposition and Schemes: A Complex Case Study
This addresses the need for trustworthy automated refactoring in industrial-scale software development, though it is incremental as it builds on existing formal verification approaches.
The paper tackles the problem of ensuring correctness in complex code refactoring tools by decomposing transformations into verifiable steps using a strategic rewriting language, resulting in semi-automatic formal verification based on programming language semantics.
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.