Towards Specification-Guarded Refactoring

Refactoring is a common task in writing and maintaining software. Refactoring tools are available for a wide variety of programming languages, and they are intended to transform source code without altering the functional behaviour of the software being refactored. However, even though most refactoring tools are designed with this criterion in mind, and programmers expect it, their implementations do not provide formal guarantees of correctness. To address this limitation, we propose a methodology for extending refactoring implementations with correctness guarantees. Our approach leverages dependently-typed languages and techniques to guard refactoring implementations with proofs of conformance to formal specifications. We illustrate our proposed methodology using a renaming refactoring that includes correctness guarantees as an integral part of its implementation.