TY  - JOUR
AU  - Brucker, Achim D.
AU  - Wolff, Burkhart
PY  - 2008//
TI  - An Extensible Encoding of Object-oriented Data Models in HOL
JO  - Journal of Automated Reasoning
SP  - 219
EP  - 249
VL  - 41
IS  - 3
PB  - Springer-Verlag
CY  - Heidelberg
KW  - object-oriented data models, HOL, theorem proving, verification
N2  - We present an extensible encoding of object-oriented data models into HOL. Our encoding is supported by a datatype package that leverages the use of the 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.
SN  - 0168-7433
UR  - http://www.brucker.ch/bibliography/abstract/brucker.ea-extensible-2008-b
L1  - http://www.brucker.ch/bibliography/download/2008/brucker.ea-extensible-2008-b.pdf
UR  - http://dx.doi.org/10.1007/s10817-008-9108-3
ID  - brucker.ea:extensible:2008-b
ER  -