Local mirror of Featherweight OCL entry of the Archive of Formal Proofs (AFP).
https://www.isa-afp.org/entries/Featherweight_OCL.shtml
You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
86 lines
4.6 KiB
86 lines
4.6 KiB
To cite the use of this formal theory, please use
|
|
|
|
Achim D. Brucker, Frédéric Tuong, and Burkhart Wolff. Featherweight
|
|
OCL: A Proposal for a Machine-Checked Formal Semantics for OCL
|
|
2.5. In Archive of Formal Proofs,
|
|
2014. http://www.isa-afp.org/entries/Featherweight_OCL.shtml, Formal
|
|
proof development
|
|
|
|
A BibTeX entry for LaTeX users is
|
|
|
|
@Article{ brucker.ea:featherweight:2014,
|
|
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 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.},
|
|
author = {Achim D. Brucker and Fr{\'e}d{\'e}ric Tuong and Burkhart Wolff},
|
|
file = {https://www.brucker.ch/bibliography/download/2014/brucker.ea-featherweight-outline-2014.pdf},
|
|
filelabel= {Outline},
|
|
issn = {2150-914x},
|
|
journal = {Archive of Formal Proofs},
|
|
month = {jan},
|
|
note = {\url{http://www.isa-afp.org/entries/Featherweight_OCL.shtml}, Formal proof development},
|
|
pdf = {https://www.brucker.ch/bibliography/download/2014/brucker.ea-featherweight-2014.pdf},
|
|
title = {Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5},
|
|
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-featherweight-2014},
|
|
year = {2014},
|
|
}
|
|
|
|
|
|
An overview of the formalization is given in:
|
|
|
|
Achim D. Brucker and Burkhart Wolff. Featherweight OCL: A study for
|
|
the consistent semantics of OCL 2.3 in HOL. In Workshop on OCL and
|
|
Textual Modelling (OCL 2012). , pages 19-24, 2012. The semantics for
|
|
the Boolean operators proposed in this paper was adopted by the OCL
|
|
2.4 standard.
|
|
|
|
A BibTeX entry for LaTeX users is
|
|
|
|
@InProceedings{ brucker.ea:featherweight:2012,
|
|
abstract = {At its origins, OCL was conceived as a strict
|
|
semantics for undefinedness, with the exception of the
|
|
logical connectives of type Boolean that constitute a
|
|
three-valued propositional logic. Recent versions of
|
|
the OCL standard added a second exception element,
|
|
which, similar to the null references in programming
|
|
languages, is given a non-strict semantics.\\\\In this
|
|
paper, we report on our results in formalizing the
|
|
core of OCL in higher-order logic (HOL). This
|
|
formalization revealed several inconsistencies and
|
|
contradictions in the current version of the OCL
|
|
standard. These inconsistencies and contradictions are
|
|
reflected in the challenge to define and implement OCL
|
|
tools (e.g., interpreters, code-generators, or theorem
|
|
provers) in a uniform manner.},
|
|
|
|
author = {Achim D. Brucker and Burkhart Wolff},
|
|
booktitle= {Workshop on OCL and Textual Modelling (OCL 2012)},
|
|
doi = {10.1145/2428516.2428520},
|
|
isbn = {978-1-4503-1799-3},
|
|
keywords = {OCL, HOL-OCL, formal semantics},
|
|
note = {The semantics for the Boolean operators proposed in this paper
|
|
was adopted by the OCL 2.4 standard.},
|
|
pages = {19--24},
|
|
pdf = {https://www.brucker.ch/bibliography/download/2012/brucker.ea-featherweight-2012.pdf},
|
|
talk = {talk:brucker.ea:featherweight:2012},
|
|
title = {Featherweight OCL: A study for the consistent semantics of OCL 2.3 in HOL},
|
|
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-featherweight-2012},
|
|
year = {2012},
|
|
}
|