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 prepositional
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.
Keywords: UML, OCL, formal methods, refactoring, requirements tracing.
