Featherweight OCL: A study for the consistent semantics of OCL 2.3 in HOL

By Achim D. Brucker and Burkhart Wolff.

At its origins, OCL was conceived as a strict semantics for undefinedness, with the exception of the logical connectives of type Boolean that constitute a three-valued propositional logic. Recent versions of the OCL standard added a second exception element, which, similar to the null references in programming languages, is given a non-strict semantics.

In this paper, we report on our results in formalizing the core of OCL in higher-order logic (HOL). This formalization revealed several inconsistencies and contradictions in the current version of the OCL standard. These inconsistencies and contradictions are reflected in the challenge to define and implement OCL tools (e.g., interpreters, code-generators, or theorem provers) in a uniform manner.

Keywords:
OCL, HOL-OCL, Formal Semantics

Supplementary material:
[ Slides  ]

Please cite this work as follows:
A. D. Brucker and B. Wolff, “Featherweight OCL: A study for the consistent semantics of OCL 2.3 in HOL,” in Workshop on OCL and textual modelling (OCL 2012), 2012, pp. 19–24. doi: 10.1145/2428516.2428520. The semantics for the Boolean operators proposed in this paper was adopted by the OCL 2.4 standard.. Author copy: http://logicalhacking.com/publications/brucker.ea-featherweight-2012/

BibTeX
@InProceedings{ brucker.ea:featherweight:2012,
  author    = {Achim D. Brucker and Burkhart Wolff},
  title     = {Featherweight {OCL}: A study for the consistent semantics of
               {OCL} 2.3 in {HOL}},
  booktitle = {Workshop on OCL and Textual Modelling (OCL 2012)},
  year      = {2012},
  abstract  = {At its origins, OCL was conceived as a strict semantics for
               undefinedness, with the exception of the logical connectives
               of type Boolean that constitute a three-valued propositional
               logic. Recent versions of the OCL standard added a second
               exception element, which, similar to the null references in
               programming languages, is given a non-strict semantics.
               
               In this paper, we report on our results in formalizing the
               core of OCL in higher-order logic (HOL). This formalization
               revealed several inconsistencies and contradictions in the
               current version of the OCL standard. These inconsistencies and
               contradictions are reflected in the challenge to define and
               implement OCL tools (e.g., interpreters, code-generators, or
               theorem provers) in a uniform manner.},
  note      = {The semantics for the Boolean operators proposed in this
               paper was adopted by the OCL 2.4 standard.. 
               Author copy: \url{http://logicalhacking.com/publications/brucker.ea-featherweight-2012/}},
  isbn      = {978-1-4503-1799-3},
  doi       = {10.1145/2428516.2428520},
  pages     = {19--24},
  areas     = {formal methods, software},
  keywords  = {OCL, HOL-OCL, Formal Semantics},
}