Abstract

Refactoring is the process of restructuring programs by means of behaviour-preserving program transformations, themselves called refactorings. Most modern development environments come with built-in support for automated refactorings that the user can perform at the push of a button. Implementing refactorings is notoriously complex, however, and even state-of-the-art implementations have very low standards of correctness.

We give an overview of our recent work on developing concepts and techniques that make it possible to give concise and modular specifications of refactorings. Our approach is based on static semantic dependencies, which express program properties to be preserved by the refactoring; decomposition of large refactorings into smaller microrefactorings, which can be developed and reused independently; and language restrictions and extensions, which abstract from the complexities of the object language.

The specifications we obtain are precise enough to cover all details of the object language, and thus give rise to full featured, high-quality refactoring implementations. Their modularity, on the other hand, makes them amenable to formal proof, and hence opens the door to the rigorous verification of refactorings.