An Interactive Proof Environment for Object-oriented Specifications

by Achim D. Brucker

Cover for brucker:interactive:2007.We present a semantic framework for object-oriented specification languages. We develop this framework as a conservative shallow embedding in Isabelle/HOL. Using only conservative extensions guarantees by construction the consistency of our formalization. Moreover, we show how our framework can be used to build an interactive proof environment, called HOL-OCL, for object-oriented specifications in general and for UML/OCL in particular.

Our main contributions are an extensible encoding of object-oriented data structures in HOL, a datatype package for object-oriented specifications, and the development of several equational and tableaux calculi for object-oriented specifications. Further, we show that our formal framework can be the basis of a formal machine-checked semantics for OCL that is compliant to the OCL 2.0 standard.

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

QR Code for brucker:interactive:2007.Please cite this article as follows:
Achim D. Brucker. An Interactive Proof Environment for Object-oriented Specifications. ETH Zurich,2007. ETH Dissertation No. 17097.
Keywords: OCL, UML, formal semantics, theorem proving, Isabelle, HOL-OCL
(full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (Share article on LinkedIn. Share article on CiteULike. )

BibTeX
@PhDThesis{ brucker:interactive:2007,
abstract = {We present a semantic framework for object-oriented specification languages. We develop this framework as a conservative shallow embedding in Isabelle/HOL. Using only conservative extensions guarantees by construction the consistency of our formalization. Moreover, we show how our framework can be used to build an interactive proof environment, called HOL-OCL, for object-oriented specifications in general and for UML/OCL in particular.\\\\Our main contributions are an extensible encoding of object-oriented data structures in HOL, a datatype package for object-oriented specifications, and the development of several equational and tableaux calculi for object-oriented specifications. Further, we show that our formal framework can be the basis of a formal machine-checked semantics for OCL that is compliant to the OCL 2.0 standard.},
abstract_de = {In dieser Arbeit wird ein semantisches Rahmenwerk f{\"u}r objektorientierte Spezifikationen vorgestellt. Das Rahmenwerk ist als konservative, flache Einbettung in Isabelle/HOL realisiert. Durch die Beschr{\"a}nkung auf konservative Erweiterungen kann die logische Konsistenz der Einbettung garantiert werden. Das semantische Rahmenwerk wird verwendet, um das interaktives Beweissystem HOL-OCL f{\"u}r objektorientierte Spezifikationen im Allgemeinen und insbesondere f{\"u}r UML/OCL zu entwickeln.\\\\Die Hauptbeitr{\"a}ge dieser Arbeit sind die Entwicklung einer erweiterbaren Kodierung objektorientierter Datenstrukturen in HOL, ein Datentyp-Paket f{\"u}r objektorientierte Spezifikationen und die Entwicklung verschiedener Kalk{\"u}le f{\"u}r objektorientierte Spezifikationen. Zudem zeigen wir, wie das formale Rahmenwerk verwendet werden kann, um eine formale, maschinell gepr{\"u}fte Semantik f{\"u}r OCL anzugeben, die konform zum Standard f{\"u}r OCL 2.0 ist.},
author = {Achim D. Brucker},
keywords = {OCL, UML, formal semantics, theorem proving, Isabelle, HOL-OCL},
month = {mar},
note = {ETH Dissertation No. 17097.},
pdf = {https://www.brucker.ch/bibliography/download/2007/brucker-interactive-2007.pdf},
school = {ETH Zurich},
title = {An Interactive Proof Environment for Object-oriented Specifications},
url = {https://www.brucker.ch/bibliography/abstract/brucker-interactive-2007},
year = {2007},
}