Object-oriented verification based on record subtyping in higher-order logic

Abstract

We show how extensible records with structural subtyping can be represented directly in Higher-Order Logic (HOL). Exploiting some specific properties of HOL, this encoding turns out to be extremely simple. In particular, structural subtyping is subsumed by naive parametric polymorphism, while overridable generic functions may be based on overloading. Taking HOL plus extensible records as a starting point, we then set out to build an environment for object-oriented specification and verification (HOOL). This framework offers several well-known concepts like classes, objects, methods and late-binding. All of this is achieved by very simple means within HOL.