Redesign of UML class diagrams: a formal approach

Contracts provide a precise way of specifying object-oriented systems. When a class structure is modified, the corresponding contracts must be modified accordingly. This paper presents a method of transforming contracts, which allows the extension of a mapping defined on a few model elements, to—what we call—an interpretation function, and to use this function to automatically translate OCL-constraints. Interestingly, such functions preserve reasoning using propositional calculi, resolution, equations, and induction. Interpretation functions can be used to trace model elements throughout multiple redesigns of UML class diagrams in both the forward, and the backward direction. The applicability of our approach is demonstrated in several examples, including some of Fowler’s refactoring patterns.