An Extensible Encoding of Object-oriented Data Models in HOL with an Application to IMP++

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 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. In: Journal of Automated Reasoning (JAR), DOI: 10.1007/s10817-008-9108-3, 41 (3-4), pages 219-249, Springer. 2008.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2008, 41 (3), pp.219-249. 〈http://link.springer.com/article/10.1007%2Fs10817-008-9108-3〉. 〈10.1007/s10817-008-9108-3〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01214567
Contributeur : Burkhart Wolff <>
Soumis le : lundi 12 octobre 2015 - 15:22:42
Dernière modification le : jeudi 11 janvier 2018 - 06:27:34

Identifiants

Collections

Citation

Achim D. Brucker, Burkhart Wolff. An Extensible Encoding of Object-oriented Data Models in HOL with an Application to IMP++. Journal of Automated Reasoning, Springer Verlag, 2008, 41 (3), pp.219-249. 〈http://link.springer.com/article/10.1007%2Fs10817-008-9108-3〉. 〈10.1007/s10817-008-9108-3〉. 〈hal-01214567〉

Partager

Métriques

Consultations de la notice

48