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

International audienceThe Unified Modeling Language (UML) is one of the few modelinglanguages that is widely used in industry. While UML is mostly knownas diagrammatic modeling language (e.g., visualizing class models), itis complemented by a textual language, called Object ConstraintLanguage (OCL). The current version of OCL is based on a four-valuedlogic that turns UML into a formal language. Any type comprises theelements "invalid" and "null" which are propagated as strict andnon-strict, respectively. Unfortunately, the former semi-formalsemantics of this specification language, captured in the "Annex A" ofthe OCL standard, leads to different interpretations of cornercases. We formalize the core of OCL: denotational definitions, alogical calculus and operational rules that allow for the execution ofOCL expressions by a mixture of term rewriting and codecompilation. Our formalization reveals several inconsistencies andcontradictions in the current version of the OCL standard. Overall,this document is intended to provide the basis for a machine-checkedtext "Annex A" of the OCL standard targeting at tool implementors