Email Gateway (Aug 19 2022 at 13:32): Email Gateway (Aug 19 2022 at 13:32):From: Lawrence Paulson <lp15@cam.ac.uk>
Many thanks to Achim D. Brucker, Frédéric Tuong and Burkhart Wolff for their entry
Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5
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 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. We formalize the core of OCL: 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. Our formalization reveals several inconsistencies and contradictions in the current version of the OCL standard. Overall, this document is intended to provide the basis for a machine-checked text "Annex A" of the OCL standard targeting at tool implementors.
Larry Paulson
Last updated: Apr 25 2024 at 20:15 UTC