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.

Further Reading:
This presentation is based on the following publication:
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: https://logicalhacking.com/publications/brucker.ea-featherweight-2012/

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,” Sep. 30, 2012. Author copy: https://logicalhacking.com/publications/talk-brucker.ea-featherweight-2012/

BibTeX
@Unpublished{ talk:brucker.ea:featherweight:2012,
  date              = {2012-09-30},
  title             = {Featherweight {OCL}: A study for the consistent semantics of
                       {OCL} 2.3 in {HOL}},
  author            = {Achim D. Brucker and Burkhart Wolff},
  eventttitle       = {Workshop on {OCL} and Textual Modelling ({OCL 2012})},
  slideshare        = {26212562},
  slideshare_width  = {427},
  slideshare_height = {356},
  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              = {Author copy: \url{https://logicalhacking.com/publications/talk-brucker.ea-featherweight-2012/}},
  pdf               = {https://logicalhacking.com/publications/talk-brucker.ea-featherweight-2012/talk-brucker.ea-featherweight-2012.pdf},
}