%0 Thesis
%T An Interactive Proof Environment for Object-oriented Specifications
%A Brucker, Achim D.
%D 2007
%8 mar
%C ETH Zurich
%F brucker:interactive:2007
%O ETH Dissertation No. 17097.
%X 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. 
%K OCL, UML, formal semantics, theorem proving, Isabelle, HOL-OCL
%9 Ph.D. thesis
%U http://www.brucker.ch/bibliography/abstract/brucker-interactive-2007
%U http://www.brucker.ch/bibliography/download/2007/brucker-interactive-2007.pdf