An Extensible Encoding of Object-oriented Data Models in HOL

By Achim D. Brucker and Burkhart Wolff.

We present an extensible encoding of object-oriented data models into HOL. Our encoding is supported by a datatype package that leverages the use of the shallow embedding technique to object-oriented specification and programming languages. The package incrementally compiles an object-oriented data model, i.e., a class model, to a theory containing object-universes, constructors, accessor functions, coercions (casts) between dynamic and static types, characteristic sets, and co-inductive class invariants. The package is conservative, i.e., all properties are derived entirely from constant definitions, including the constraints over object structures. As an application, we use the package for an object-oriented core-language called IMP++, for which we formally prove the correctness of a Hoare-Logic with respect to a denotational semantics.

Keywords:
Object-Oriented Data Models, HOL, Theorem Proving, Verification

Please cite this work as follows:
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: https://logicalhacking.com/publications/brucker.ea-extensible-2008-b/

BibTeX
@Article{ brucker.ea:extensible:2008-b,
  abstract  = {We present an extensible encoding of object-oriented data
               models into HOL. Our encoding is supported by a datatype
               package that leverages the use of the shallow embedding
               technique to object-oriented specification and programming
               languages. The package incrementally compiles an
               object-oriented data model, i.e., a class model, to a theory
               containing object-universes, constructors, accessor functions,
               coercions (casts) between dynamic and static types,
               characteristic sets, and co-inductive class invariants. The
               package is conservative, i.e., all properties are derived
               entirely from constant definitions, including the constraints
               over object structures. As an application, we use the package
               for an object-oriented core-language called IMP++, for which
               we formally prove the correctness of a Hoare-Logic with
               respect to a denotational semantics.},
  author    = {Achim D. Brucker and Burkhart Wolff},
  language  = {USenglish},
  areas     = {formal methods, software},
  keywords  = {Object-Oriented Data Models, HOL, Theorem Proving,
               Verification},
  title     = {An Extensible Encoding of Object-oriented Data Models in
               {HOL}},
  year      = {2008},
  journal   = {Journal of Automated Reasoning },
  volume    = {41},
  issue     = {3},
  pages     = {219--249},
  issn      = {0168-7433},
  doi       = {10.1007/s10817-008-9108-3},
  publisher = {Springer-Verlag },
  address   = {Heidelberg },
  note      = {Author copy: \url{https://logicalhacking.com/publications/brucker.ea-extensible-2008-b/}},
  pdf       = {https://logicalhacking.com/publications/brucker.ea-extensible-2008-b/brucker.ea-extensible-2008-b.pdf},
}