Abstract:

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

Achim D. Brucker and Burkhart Wolff


We present a datatype package that enables the use of 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 accessor functions, coercions between dynamic and static 
types, characteristic sets, their relations reflecting inheritance, and the necessary class invariants. The package is 
conservative, i.e., all properties are derived entirely from axiomatic definitions. As an application, we use the 
package for an object-oriented core-language called IMPOO, for which correctness of a Hoare logic with respect 
to an operational semantics is proven.