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

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},
}