TY  - THES
AU  - Brucker, Achim D.
PY  - 2007/mar/
TI  - An Interactive Proof Environment for Object-oriented Specifications
PB  - ETH Zurich
KW  - OCL, UML, formal semantics, theorem proving, Isabelle, HOL-OCL
N2  - 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. 
UR  - http://www.brucker.ch/bibliography/abstract/brucker-interactive-2007
L1  - http://www.brucker.ch/bibliography/download/2007/brucker-interactive-2007.pdf
N1  - ETH Dissertation No. 17097.
ID  - brucker:interactive:2007
U1  - Ph.D. thesis
ER  -