pdfreaders.org

A Package for Extensible Object-Oriented Data Models with an Application to IMP++

Achim D. Brucker und Burkhart Wolff

Cover for brucker.ea:package:2006.We present a datatype package that enables the use of 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 accessor 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 IMPOO, for which correctness of a Hoare logic with respect to an operational semantics is proven.

Schlüsselwörter: datatype package, extensible object-oriented data model, object-oriented specification,shallow embedding
Kategorien: ,
Dokumente: (Artikel als PDF Datei)

QR Code for brucker.ea:package:2006.Bitte zitieren sie diesen Artikel wie folgt:
Achim D. Brucker und Burkhart Wolff. A Package for Extensible Object-Oriented Data Models with an Application to IMP++. In International Workshop on Software Verification and Validation (SVV 2006), 2006.
Schlüsselwörter: datatype package, extensible object-oriented data model, object-oriented specification,shallow embedding
(Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (Share article on LinkedIn. Share article on CiteULike.)

BibTeX
@InCollection{ brucker.ea:package:2006,
abstract = {We present a datatype package that enables the use of 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 accessor 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 \IMPOO, for which correctness of a Hoare logic with respect to an operational semantics is proven.},
address = {Seattle, USA},
author = {Achim D. Brucker and Burkhart Wolff},
booktitle = {International Workshop on Software Verification and Validation (SVV 2006)},
editor = {Abhik Roychoudhury and Zijiang Yang},
keywords = {datatype package, extensible object-oriented data model, object-oriented specification,shallow embedding},
language = {USenglish},
month = {aug},
pdf = {https://www.brucker.ch/bibliography/download/2006/brucker.ea-package-2006.pdf},
title = {A Package for Extensible Object-Oriented Data Models with an Application to {IMP++}},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-package-2006},
year = {2006},
}