OCL (Object Constraint Language) is used everywhere: to define well-formedness rules, query expressions, model transformations,… but (as happens with most languages) a precise definition of the OCL semantics was lacking.
Indeed, the OCL standard document from the OMG does include an Appendix A with a partial formal semantics but this was useful more as a reference than as the basis to build precise OCL evaluation tools on top of it (so it was not uncommon to find that two OCL tools returned a different value when evaluating the same expression).
This week, Achim D. Brucker and Burkhart Wolff have just announced what it looks like a big step in the right direction. Their paper: Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5 is now available in the Archive of Formal Proof.
As they say: “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.”
Let’s see the OMG takes note, validates the work (should be easy, just 200 pages of formal proofs 🙂 ) and adds it to the standard.
(and for those that do not want to read the proof but want to learn the language, check our OCL tutorial)
FNR Pearl Chair. Head of the Software Engineering RDI Unit at LIST. Affiliate Professor at University of Luxembourg. More about me.
Recent Comments