Modelchecking Correctness of Refactorings - Some Experiments

Refactorings are changes made to programs, models or specifications with the intention of improving their structure and thus making them clearer, more readable and re-usable. Refactorings are required to be behaviour-preserving in that the external behaviour of the program/model/specification remains unchanged. In this paper we show how a simple type of refactorings on object-oriented specifications (written in ObjectZ) can be formally shown to be behaviour-preserving using a modelchecker (SAL). The class of refactorings treated covers those operating on a single method only.

• Type: Journal
• Year: 2007
• Where: ENTCS
• Authors: H.-Christian Estler, Thomas Ruhroth, Heike Wehrheim
• Keywords: ENTCS 2007, External Behaviour, Refactorings, Simple Type