Technical Report No. 168 - Abstract

Achim D. Brucker, Burkhart Wolff
A Note on Design Decisions of a Formalization of the OCL

We compare several formal and informal approaches to define the semantics of the Object Constraint Language (OCL). This comparison reveals a number of minor and major design problems to be settled in upcoming versions of the OCL standard. We review these problems in the context of our work of providing a formal semantics of OCL through an conservative embedding in HOL using the Isabelle theorem prover.