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

By Achim D. Brucker and Burkhart Wolff.

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 IMP++, for which correctness of a Hoare logic with respect to an operational semantics is proven.

Keywords:
Datatype Package, Extensible Object-Oriented Data Model, Object-Oriented Specification, Shallow Embedding

Please cite this work as follows:
A. D. Brucker and B. Wolff, “A package for extensible object-oriented data models with an application to IMP++,” in International workshop on software verification and validation (SVV 2006), A. Roychoudhury and Z. Yang, Eds. Seattle, USA, 2006. Author copy: https://logicalhacking.com/publications/brucker.ea-package-2006/

BibTeX
@InCollection{ brucker.ea:package:2006,
  author    = {Achim D. Brucker and Burkhart Wolff},
  title     = {A Package for Extensible Object-Oriented Data Models with an
               Application to {IMP++}},
  editor    = {Abhik Roychoudhury and Zijiang Yang},
  booktitle = {International Workshop on Software Verification and
               Validation (SVV 2006)},
  year      = {2006},
  month     = {aug},
  address   = {Seattle, USA},
  language  = {USenglish},
  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 IMP++, for which
               correctness of a Hoare logic with respect to an operational
               semantics is proven.},
  areas     = {formal methods, software},
  keywords  = {Datatype Package, Extensible Object-Oriented Data Model,
               Object-Oriented Specification, Shallow Embedding},
  note      = {Author copy: \url{https://logicalhacking.com/publications/brucker.ea-package-2006/}},
  pdf       = {https://logicalhacking.com/publications/brucker.ea-package-2006/brucker.ea-package-2006.pdf},
}