Specifying and reasoning in the calculus of objects

dissertation

English

The present thesis introduces and studies a type theoretic system equipped with the type constructor of a simple form of objects and justifies the development by showing a capability of the system for specification and refinement of functional programs. The invented interpretation of an object type requires rather a non-trivial extension of the underlaying lambda calculus. The notion of box, which is the content containment structure equipped with a marker variable, is added to the syntax of the term calculus. The acquired overall simpler notation is a justification of the need for this extraordinary extension.     The objectives of this thesis are mainly to give the formal representation of a simple object form and to show its significant metatheoretical properties. We also show the capabilities of the acquired system for specifying and reasoning about programs by defining the basic concepts for program specifications and refinement and techniques for reasoning about the correctness of programs.  To achieve this goals we introduce and formally define a type theoretic system called Core Calculus of Objects and study its basic metatheoretical properties. The significant theorems of the calculus, in particular, confluence of computations, subject reduction, strong normalization, and the reflection of equality, are established herein. These properties are important for the logical consistency of the calculus and the existence of a decidable type-checking algorithm.     Finally, a demonstration of the pragmatic use of the Calculus of Objects for specifying program modules is provided. Refinement and reuse techniques are formulated by means of specification operations known from algebraic specification languages.

type theory, object types, subtyping, object-oriented formal specification, encapsulation

RYŠAVÝ, O.

29. 9. 2005

Brno

95

http://www.fit.vutbr.cz/~rysavy/bibpdf/rysavy_04_dissertation.pdf