pdfreaders.org

Extensible Universes for Object-oriented Data Models

Achim D. Brucker und Burkhart Wolff

Cover for brucker.ea:extensible:2008.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.

Schlüsselwörter: object-oriented data models, HOL, formal methods, UML, OCL
Kategorien: ,
Dokumente: (Artikel als PDF Datei)

QR Code for brucker.ea:extensible:2008.Bitte zitieren sie diesen Artikel wie folgt:
Achim D. Brucker und Burkhart Wolff. Extensible Universes for Object-oriented Data Models. In ECOOP 2008 - Object-Oriented Programming. Lecture Notes in Computer Science (5142), pages 438-462, Springer-Verlag, 2008.
Schlüsselwörter: object-oriented data models, HOL, formal methods, UML, OCL
(Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-540-70592-5_19) (Share article on LinkedIn. Share article on CiteULike.)

BibTeX
@InCollection{ brucker.ea:extensible:2008,
abstract = {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.},
address = {Heidelberg},
author = {Achim D. Brucker and Burkhart Wolff},
booktitle = {ECOOP 2008 -- Object-Oriented Programming},
doi = {10.1007/978-3-540-70592-5_19},
editor = {Jan Vitek},
keywords = {object-oriented data models, HOL, formal methods, UML, OCL},
language = {USenglish},
location = {Paphos, Cyprus},
number = {5142},
pages = {438--462},
pdf = {https://www.brucker.ch/bibliography/download/2008/brucker.ea-extensible-2008.pdf},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
title = {Extensible Universes for Object-oriented Data Models},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-extensible-2008},
year = {2008},
}