Treffer: An Extensible Encoding of Object-oriented Data Models in <span style="font-variant:small-caps">hol</span>.

Abstract  We present an extensible encoding of object-oriented data models into higher-order logic (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 static types (and providing a foundation for the notion of dynamic 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. [ABSTRACT FROM AUTHOR]

Copyright of Journal of Automated Reasoning is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)