Trustworthy Refactoring via Decomposition and Schemes: A Complex Case Study

TL;DR

This paper introduces a method for trustworthy code refactoring that decomposes complex transformations into smaller, verifiable steps using a formal specification language and semi-automatic verification, enhancing confidence in automated refactoring tools.

Contribution

It presents a novel approach combining decomposition, refactoring schemes, and formal verification to improve correctness assurance in complex code transformations.

Findings

Decomposition into smaller steps facilitates formal verification.

Refactoring schemes enable reusable and extensible transformations.

Semi-automatic verification ensures correctness of complex refactorings.

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.