Changing Programs Correctly: Refactoring with Specifications

Refactorings change the internal structure of code without changing its external behavior. For non-trivial refactorings, the preservation of external behavior depends on semantic properties of the program that are difficult to check automatically before the refactoring is applied. Therefore, existing refactoring tools either do not support non-trivial refactorings at all or force programmers to rely on (typically incomplete) test suites to check their refactorings.

The technique presented in the paper allows one to show the preservation of external behavior even for complex refactorings. For a given refactoring, we prove once and for all that the refactoring is an equivalence transformation, provided that the refactored program satisfies certain semantic correctness conditions. These conditions can be added automatically as assertions to the refactored program and checked at runtime or verified statically. Our technique allows tools to apply even complex refactorings safely, and refactorings automatically improve program documentation by generating assertions.