The HOL-OCL Book

@TechReport{ brucker.ea:hol-ocl-book:2006,
  author      = {Achim D. Brucker and Burkhart Wolff},
  institution = {ETH Zurich},
  language    = {USenglish},
  title       = {The {HOL-OCL} Book},
  areas       = {formal methods, software},
  year        = {2006},
  number      = {525},
  abstract    = {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},
  bibkey      = {brucker.ea:hol-ocl-book:2006},
  keywords    = {Security, SecureUML, UML, OCL, HOL-OCL,
                 Model-Transformation},
  note        = {Author copy: \url{https://logicalhacking.com/publications/brucker.ea-hol-ocl-book-2006/}},
  pdf         = {https://logicalhacking.com/publications/brucker.ea-hol-ocl-book-2006/brucker.ea-hol-ocl-book-2006.pdf},
}