An Interactive Proof Environment for Object-oriented Specifications
by Achim D. Brucker
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)
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) (
| 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.}, | |
| = | {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}, |