Formalizing Refactorings Implemented in Eclipse

The Eclipse IDE is a widely used programming environment. As a result the refactorings it provides for java code are also very well known. However there is no formal definition available for eclipse’s refactoring methods. Such a formal definition could be used to compare eclipse’s implementation to others, and to prove certain properties on eclipse’s refactoring methods. This leads us to the question of whether it is feasible to formalise the refactorings that are implemented in eclipse. To answer this question the source code for a few refactorings is analysed to extract their pre- and postconditions. These pre- and postconditions are then written down in story diagrams which we found to be the most promising way of formalising refactorings. To validate that these story diagrams are equivalent to the implementation in eclipse, both the story diagrams and the refactorings in eclipse are executed