A Package for Extensible Object-Oriented Data Models with an Application to IMP++

Abstract

We present a datatype package that enables the use ofshallow embedding technique to object-orientedspecification and programming languages. The packageincrementally compiles an object-oriented data model to atheory containing object-universes, constructors, andaccessor functions, coercions between dynamic and statictypes, characteristic sets, their relations reflectinginheritance, and the necessary class invariants. Thepackage is conservative, i.e., all properties are derivedentirely from axiomatic definitions. As an application, weuse the package for an object-oriented core-language called\IMPOO, for which correctness of a Hoare logic with respectto an operational semantics is proven.