Inheritance of specifications in the calculus of functional objects

Abstract data types, formal definitions and theory, object-oriented languages, object types, program construction, type theory.

Solid theoretical foundation of object-oriented paradigm have been developed for both functional and imperative programming languages. Although type theory contains functional programming language and offers rich specification and reasoning capabilities the similar foundation is not so evident despite the presence of flavor of object orientation in many other formal methods. The idea of the present work is straightforward. Object type consists of object's interface signature specification and accompanied specification in form of logical proposition. An object value is a collection of operations working on an internal state and a proof of correctness of the implementation. In this manner, certain principles of object-orientation can be also applied to accompanied proofs, namely inheritance, late binding, and encapsulation. Paper introduces a new calculus that features object notion as a primitive construction allowing for quite simple presentation. Object type constructor combines existential and recursive types akin to Self type of Abadi and Cardelli. To simplify the presentation and to avoid introducing general fixed point constructor a special sort of expressions is introduced -- boxed expressions. A boxed expression is an expression annotated with a variable that with suitable defined substitution operation allows us to encode a restricted form of self application and positive methods.