Semantic Issues of OCL: Past, Present, and Future

By Achim D. Brucker, Jürgen Doser, and Burkhart Wolff.

We report on the results of a long-term project to formalize the semantics of OCL 2.0 in Higher-order Logic (HOL). The ultimate goal of the project is to provide a formalized, machine-checked semantic basis for a theorem proving environment for OCL (as an example for an object-oriented specification formalism) which is as faithful as possible to the original informal semantics. We report on various (minor) inconsistencies of the OCL semantics, discuss the more recent attempt to align the OCL semantics with UML 2.0 and suggest several extensions which make, in our view, OCL semantics more fit for future extensions towards programming-like verifications and specification refinement, which are, in our view, necessary to make OCL more fit for future extensions.

Keywords:
HOL-OCL, UML/OCL, Formal Semantics

Supplementary material:
[ Slides  ]

Please cite this work as follows:
A. D. Brucker, J. Doser, and B. Wolff, “Semantic issues of OCL: Past, present, and future,” Electronic Communications of the EASST, vol. 5, 2006, doi: 10.14279/tuj.eceasst.5.46. Author copy: https://logicalhacking.com/publications/brucker.ea-semantic-2006-b/

BibTeX
@Article{ brucker.ea:semantic:2006-b,
  abstract = {We report on the results of a long-term project to formalize
              the semantics of OCL 2.0 in Higher-order Logic (HOL). The
              ultimate goal of the project is to provide a formalized,
              machine-checked semantic basis for a theorem proving
              environment for OCL (as an example for an object-oriented
              specification formalism) which is as faithful as possible to
              the original informal semantics. We report on various (minor)
              inconsistencies of the OCL semantics, discuss the more recent
              attempt to align the OCL semantics with UML 2.0 and suggest
              several extensions which make, in our view, OCL semantics more
              fit for future extensions towards programming-like
              verifications and specification refinement, which are, in our
              view, necessary to make OCL more fit for future extensions.},
  author   = {Achim D. Brucker and J\"urgen Doser and Burkhart Wolff},
  language = {USenglish},
  areas    = {formal methods, software},
  keywords = {HOL-OCL, UML/OCL, Formal Semantics},
  title    = {Semantic Issues of {OCL}: Past, Present, and Future},
  editor   = {Birgith Demuth and Dan Chiorean and Martin Gogolla and Jos
              Warmer},
  issn     = {1863-2122},
  volume   = {5},
  year     = {2006},
  journal  = {Electronic Communications of the EASST },
  doi      = {10.14279/tuj.eceasst.5.46},
  note     = {Author copy: \url{https://logicalhacking.com/publications/brucker.ea-semantic-2006-b/}},
  pdf      = {https://logicalhacking.com/publications/brucker.ea-semantic-2006-b/brucker.ea-semantic-2006-b.pdf},
}