Translating the Object Constraint Language into First-order Predicate Logic

Abstract. In this paper, we define a translation of UML class diagrams with OCL constraints into first-order predicate logic. The goal is logical reasoning about UML models, realized by an interactive theorem prover. We put an emphasis on usability of the formulas resulting from the translation, and we have developed optimisations and heuristics to enhance the efficiency of the theorem proving process. The translation has been implemented as part of the KeY system, but our implementation can also be used stand-alone.