Refactoring Object-Oriented Specifications with Data and Processes

Abstract. Refactoring is a method for improving the structure of pro-grams/specifications as to enhance readability, modularity and reusabil-ity. Refactorings are required to be behaviour-preserving in that – to an external observer – no difference between the program before and after refactoring is visible. In this paper, we develop refactorings for an object-oriented specification formalism combining a state-based lan-guage (Object-Z) with a process algebra (CSP). In contrast to OO-programming languages, refactorings moving methods or attributes up and down the class hierarchy, in addition, need to change CSP processes. We formally prove behaviour preservation with respect to the failures-divergences model of CSP.