We present a datatype package that enables the shallow embedding technique to object-oriented specification and programming languages. This datatype package incrementally compiles an object-oriented data model to a theory containing object-universes, constructors, 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. © 2008 Springer-Verlag.
CITATION STYLE
Brucker, A. D., & Wolff, B. (2008). Extensible universes for object-oriented data models. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5142 LNCS, pp. 438–462). https://doi.org/10.1007/978-3-540-70592-5_19
Mendeley helps you to discover research relevant for your work.