pdfreaders.org

Featherweight OCL: A study for the consistent semantics of OCL 2.3 in HOL

Achim D. Brucker und Burkhart Wolff

Cover for brucker.ea:featherweight:2012.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.

Schlüsselwörter: OCL, HOL-OCL, formal semantics
Kategorien: ,
Dokumente: (Artikel als PDF Datei) (Folien) (Handout)

QR Code for brucker.ea:featherweight:2012.Bitte zitieren sie diesen Artikel wie folgt:
Achim D. Brucker und 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.
Schlüsselwörter: OCL, HOL-OCL, formal semantics
(Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1145/2428516.2428520) (Share article on LinkedIn. Share article on CiteULike.)

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