Formalising behaviour preserving program transformations

The notion of refactoring-transforming the source-code of an object-oriented program without changing its external behaviour has increased the need for a precise definition of refactorings and their properties. This paper introduces a graph representation of those aspects of the source code that should be preserved by a refactoring, and graph rewriting rules as a formal specification for the refactoring transformations themselves. To this aim, we use type graphs, forbidden subgraphs, embedding mechansims, negative application conditions and controlled graph rewriting. We show that it is feasible to reason about the effect of refactorings on object-oriented programs independently of the programming language being used. This is crucial for the next generation of refactoring tools.