Verification of Refactorings in Isabelle/HOL

Refactorings are source-to-source behaviour-preserving program transformations that are used for improving program structure. Programmers refactor code to adapt it when new functionality is added or when the code is being repaired -- refactoring serves to keep the code ``clean'' and more maintainable. Refactoring can also be used as an exploratory technique for understanding source code. The process of refactoring has been automated through the implementation of tools; these tools assist programmers by handling the consistent application of behaviour-preserving changes to the code. It is desirable that the implementations of refactorings are correct: bugs might otherwise be introduced in refactored programs. The correctness, i.e. behaviour-preservation, of refactoring is traditionally probed by testing the refactored program and not the refactoring implementation directly. Recently, automated testing techniques have been used to test implementations of refactorings directly, but the coverage of testing is partial at best. The verification of refactorings is more challenging but determines whether a refactoring is behaviour-preserving for all possible programs. We study the verification of refactorings using the proof assistant Isabelle/HOL for untyped and typed lambda-calculi. Some of the issues encountered during verification are technical rather than purely theoretical: they relate to the embedding of the programming language in the proof environment. The reasons for our choice of techniques are discussed. We also discuss other practical considerations such as the readability of mechanised refactorings, and the avoidance of computationally expensive refactorings.