Abstract:

The HOL-OCL Book

Achim D. Brucker and Burkhart Wolff



HOL-OCL is an interactive proof environment for the Object Constraint Language (OCL). It is implemented as 
a shallow embedding of OCL into the Higher-order Logic (HOL) instance of the interactive theorem prover 
Isabelle. HOL-OCL defines a machine-checked formalization of the semantics as described in the standard for 
OCL 2.0. This conservative, shallow embedding of UML/OCL into Isabelle/HOL includes support for typed, 
extensible UML data models supporting inheritance and subtyping inside the typed lambda-calculus with 
parametric polymorphism. As a consequence of conservativity with respect to higher-order logic (HOL), we 
can guarantee the consistency of the semantic model. Moreover, HOL-OCL provides several derived calculi 
for UML/OCL that allow for formal derivations establishing the validity of UML/OCL formulae. Elementary 
automated support for such proofs is also provided top