| Extensible Object-oriented Data Models in Isabelle/HOL (2008) | |||||||||||||||
Abstract | |||||||||||||||
| 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 enables 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 system, to a theory containing object-universes, constructors, and accessor functions, coercions (casts) between dynamic and static types, characteristic sets, their relations reflecting inheritance, and co-inductive class invariants. The package is conservative, i. e., all properties are derived entirely from constant definitions. As an application, we show constraints over object structures. 1 | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||