Detail publikace

Specifying and reasoning in the calculus of objects

RYŠAVÝ, O.

Originální název

Specifying and reasoning in the calculus of objects

Typ

dizertace

Jazyk

angličtina

Originální abstrakt

Since type theory merges constructive logic with functional programming language it appears a very promising system for formal program construction. The present thesis deals with this idea in the environment of a type theoretic system equipped with the type constructor representing a simple form of objects. The interpretation of object type in a type theoretic system requires rather non-trivial extension of the underlaying lambda calculus. The notion of box, which is the content containment structure with a marker variable, is added to the syntax of the calculus that allows to separate the internal state of objects in the expressions. The acquired overall simple notation is a justification of the need for this extraordinary extension. The objectives of this thesis are mainly to give the formal representation of simple object model and to show its significant metatheoretical properties. We also show the capabilities of the system for specifying and reasoning about programs by defining the basic concepts of program specifications and several stewise refinement operations and techniques for reasoning about the correctness of programs. To do this the Core Calculus of Objects (CCO) is introduced. CCO is derived from ECC by stripping out Sigma-types and adding object types. The basic metatheoretical properties of the Core Calculus of Object is studied. The significant theorems of the calculus, in particular the confluence of the computation, subject reduction, strong normalization, and the reflection of equality, are proven. 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 several specification operations known from algebraic specification languages.

Klíčová slova

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

Autoři

RYŠAVÝ, O.

Vydáno

29. 9. 2005

Místo

Brno

Strany počet

95

BibTex

@phdthesis{BUT66770,
  author="Ondřej {Ryšavý}",
  title="Specifying and reasoning in the calculus of objects",
  address="Brno",
  pages="95",
  year="2005"
}