Abstract


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.