Extensible Object-Theories in HOL-OCL

We present a datatype package that enables the shallow embedding technique to object-oriented specification and programming languages. The package incrementally compiles an object-oriented data model to a theory containing object-universes, constructors, and accessors functions, coercions between dynamic and static types, class invariants, and their relations reflecting inheritance. The package is conservative, i.e., all properties are derived entirely from axiomatic definitions. As an application, we use the package for a object-oriented core-language called IMP++, for which correctness of a Hoare-Logic with respect to an operational semantics is proven.