A Note on Design Decisions of a Formalization of the OCL

By Achim D. Brucker and Burkhart Wolff.

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 a conservative embedding in HOL using the Isabelle theorem prover.

Keywords:
UML, OCL, Formal Semantics, HOL, Isabelle

Please cite this work as follows:
A. D. Brucker and B. Wolff, “A note on design decisions of a formalization of the OCL,” Albert-Ludwigs-Universität Freiburg, 168, Jan. 2002. Author copy: http://logicalhacking.com/publications/brucker.ea-note-2002/

BibTeX
@TechReport{ brucker.ea:note:2002,
  author      = {Achim D. Brucker and Burkhart Wolff},
  institution = {Albert-Ludwigs-Universit{\"a}t Freiburg},
  language    = {USenglish},
  month       = {jan},
  title       = {A Note on Design Decisions of a Formalization of the {OCL}},
  abstract    = {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 a conservative embedding in
                 HOL using the Isabelle theorem prover.},
  keywords    = {UML, OCL, Formal Semantics, HOL, Isabelle},
  areas       = {formal methods, software},
  year        = {2002},
  number      = {168},
  note        = {Author copy: \url{http://logicalhacking.com/publications/brucker.ea-note-2002/}},
}