A Note on Design Decisions of a Formalization of the OCL

by Achim D. Brucker and Burkhart Wolff

Cover for brucker.ea:note:2002.We compare several formal and informal approaches to define the semantics of the Object Constraint Language (OCL). This comparison reveals a number of minor and major design problems to be settled in upcoming versions of the OCL standard. We review these problems in the context of our work of providing a formal semantics of OCL through an conservative embedding in HOL using the Isabelle theorem prover.

Keywords: UML, OCL, formal semantics, HOL, Isabelle
Categories: ,
Documents: (full text as PDF file)

QR Code for brucker.ea:note:2002.Please cite this article as follows:
Achim D. Brucker and Burkhart Wolff. A Note on Design Decisions of a Formalization of the OCL. Albert-Ludwigs-Universität Freiburg, Technical Report 168, 2002.
Keywords: UML, OCL, formal semantics, HOL, Isabelle
(full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (Share article on LinkedIn. Share article on CiteULike. )

BibTeX
@TechReport{ brucker.ea:note:2002,
abstract = {We compare several formal and informal approaches to define the semantics of the Object Constraint Language (OCL). This comparison reveals a number of minor and major design problems to be settled in upcoming versions of the OCL standard. We review these problems in the context of our work of providing a formal semantics of OCL through an conservative embedding in HOL using the Isabelle theorem prover.},
author = {Achim D. Brucker and Burkhart Wolff},
institution = {Albert-Ludwigs-Universit{\"a}t Freiburg},
keywords = {UML, OCL, formal semantics, HOL, Isabelle},
language = {USenglish},
month = {jan},
number = {168},
pdf = {https://www.brucker.ch/bibliography/download/2002/brucker.ea-note-2002.pdf},
title = {A Note on Design Decisions of a Formalization of the {OCL}},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-note-2002},
year = {2002},
}