An Interactive Proof Environment for Object-oriented Specifications

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

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
(PDF) (BibTeX) (Endnote) (RIS) ( )