Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5

@TechReport{ brucker.ea:formal-semantics-ocl-2.5:2015,
  author      = {Achim D. Brucker and Fr{\'e}d{\'e}ric Tuong and Burkhart
                 Wolff},
  institution = {LRI, Univ Paris Sud, CNRS, Centrale Sup\'elec, Universit\'e
                 Paris-Saclay, France},
  language    = {USenglish},
  month       = {sep},
  title       = {Featherweight OCL: A Proposal for a Machine-Checked Formal
                 Semantics for OCL 2.5},
  areas       = {formal methods, software},
  year        = {2015},
  number      = {1582},
  num_pages   = {196},
  abstract    = {The Unified Modeling Language (UML) is one of the few
                 modeling languages that is widely used in industry. While UML
                 is mostly known as diagrammatic modeling language (e.g.,
                 visualizing class models), it is complemented by a textual
                 language, called Object Constraint Language (OCL). OCL is a
                 textual annotation language, originally based on a
                 three-valued logic, that turns UML into a formal language.
                 Unfortunately the semantics of this specification language,
                 captured in the ``Annex A'' of the OCL standard, leads to
                 different interpretations of corner cases. Many of these
                 corner cases had been subject to formal analysis since more
                 than ten years.
                 
                 The situation complicated with the arrival of version 2.3 of
                 the OCL standard. OCL was aligned with the latest version of
                 UML: this led to the extension of the three-valued logic by a
                 second exception element, called null. While the first
                 exception element invalid has a strict semantics, null has a
                 non strict interpretation. The combination of these semantic
                 features lead to remarkable confusion for implementors of OCL
                 compilers and interpreters.
                 
                 In this paper, we provide a formalization of the core of OCL
                 in HOL. It provides denotational definitions, a logical
                 calculus and operational rules that allow for the execution of
                 OCL expressions by a mixture of term rewriting and code
                 compilation. Moreover, we describe a coding-scheme for UML
                 class models that were annotated by code-invariants and code
                 contracts. An implementation of this coding-scheme has been
                 undertaken: it consists of a kind of compiler that takes a UML
                 class model and translates it into a family of definitions and
                 derived theorems over them capturing the properties of
                 constructors and selectors, tests and casts resulting from the
                 class model. However, this compiler is not included in this
                 document.
                 
                 Our formalization reveals several inconsistencies and
                 contradictions in the current version of the OCL standard.
                 They reflect a challenge to define and implement OCL tools in
                 a uniform manner. Overall, this document is intended to
                 provide the basis for a machine-checked text ``Annex A'' of
                 the OCL standard targeting at tool implementors.},
  note        = {Author copy: \url{https://logicalhacking.com/publications/brucker.ea-formal-semantics-ocl-2.5-2015/}},
  pdf         = {https://logicalhacking.com/publications/brucker.ea-formal-semantics-ocl-2.5-2015/brucker.ea-formal-semantics-ocl-2.5-2015.pdf},
}