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). The current version of OCL is based on a four-valued
logic that turns UML into a formal language. Any type
comprises the elements "invalid" and "null" which are
propagated as strict and non-strict, respectively.
Unfortunately, the former semi-formal 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. |
BibTeX: |
@article{Featherweight_OCL-AFP,
author = {Achim D. Brucker and Frédéric Tuong and Burkhart Wolff},
title = {Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5},
journal = {Archive of Formal Proofs},
month = jan,
year = 2014,
note = {\url{https://isa-afp.org/entries/Featherweight_OCL.html},
Formal proof development},
ISSN = {2150-914x},
}
|