Abstract:


An Extensible Encoding of Object-oriented Data Models 
in HOL with an Application to IMP++



Achim D. Brucker and Burkhart Wolff




We present an extensible encoding of object-oriented 
data models into higher-order logic (HOL). Our encoding 
is supported by a datatype package that leverages the 
use ofthe shallow embedding technique to object-oriented 
specification and programming languages. The package 
incrementally compiles an object-oriented data model, 
i.e.,a class model, to a theory containing object-
universes,constructors, accessor functions, coercions 
(casts) between dynamic and static types, characteristic 
sets, and co-inductive class invariants. The package is 
conservative,i. e., all properties are derived entirely 
from constant definitions, including the constraints over 
object structures. As an application, we use the package 
for an object-oriented core-language called IMP++, for 
which we formally prove the correctness of a Hoare logic 
with respect to a denotational semantics.