Extensible Universes for Object-oriented Data Models

By Achim D. Brucker and Burkhart Wolff.

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.

Keywords:
Object-Oriented Data Models, HOL, Formal Methods, UML, OCL

Obsoleted by:
This publication has been obsoleted by the following publication:
A. D. Brucker and B. Wolff, “An extensible encoding of object-oriented data models in HOL,” Journal of Automated Reasoning, vol. 41, pp. 219–249, 2008, doi: 10.1007/s10817-008-9108-3. Author copy: http://logicalhacking.com/publications/brucker.ea-extensible-2008-b/

Please cite this work as follows:
A. D. Brucker and B. Wolff, “Extensible universes for object-oriented data models,” in ECOOP 2008 – object-oriented programming, J. Vitek, Ed. Heidelberg: Springer-Verlag, 2008, pp. 438–462. doi: 10.1007/978-3-540-70592-5_19. Author copy: http://logicalhacking.com/publications/brucker.ea-extensible-2008/

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.},
  location    = {Paphos, Cyprus},
  author      = {Achim D. Brucker and Burkhart Wolff},
  booktitle   = {ECOOP 2008 -- Object-Oriented Programming},
  language    = {USenglish},
  publisher   = {Springer-Verlag },
  address     = {Heidelberg },
  series      = {Lecture Notes in Computer Science },
  doi         = {10.1007/978-3-540-70592-5_19},
  obsoletedby = {brucker.ea:extensible:2008-b},
  title       = {Extensible Universes for Object-oriented Data Models},
  number      = {5142},
  pages       = {438--462},
  areas       = {formal methods, software},
  keywords    = {Object-Oriented Data Models, HOL, Formal Methods, UML, OCL},
  year        = {2008},
  editor      = {Jan Vitek},
  note        = {Author copy: \url{http://logicalhacking.com/publications/brucker.ea-extensible-2008/}},
}