TY  - CHAP
AU  - Brucker, Achim D.
AU  - Wolff, Burkhart
ED  - Vitek, Jan
PY  - 2008//
TI  - Extensible Universes for Object-oriented Data Models
BT  - ECOOP 2008 ? Object-Oriented Programming
T3  - Lecture Notes in Computer Science
SP  - 438
EP  - 462
IS  - 5142
PB  - Springer-Verlag
CY  - Heidelberg
KW  - object-oriented data models, HOL, formal methods, UML, OCL
N2  - 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, 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 IMP++, for which correctness of a Hoare-Logic with respect to an operational semantics is proven. 
UR  - http://www.brucker.ch/bibliography/abstract/brucker.ea-extensible-2008
L1  - http://www.brucker.ch/bibliography/download/2008/brucker.ea-extensible-2008.pdf
UR  - http://dx.doi.org/10.1007/978-3-540-70592-5_19
ID  - brucker.ea:extensible:2008
ER  -