[Prev][Next][Index][Thread]

A Type-Theoretic Basis for an Object-Oriented Refinement Calculus


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

This is to announce the availability of the paper

    A Type-Theoretic Basis for an Object-Oriented Refinement Calculus

by

    ftp://ftp.abo.fi/pub/cs/papers/emil/oorefcalc.ps.gz

or via my Web page:

    http://www.abo.fi/~esekerin

A longer abstract of the paper follows.

Emil Sekerinski

Abo Akademi, Department of Computer Science
Lemminkaisenkatu 14 A, 20520 Turku, Finland

-------------------------------------------------------------------------
Abstract

This paper addresses the issue of giving a formal semantics to an
object-oriented programming and specification language. Object-oriented
constructs considered are objects with attributes and methods,
encapsulation of attributes, subtyping, bounded type parameters,
classes, and inheritance. Classes are distinguished from object types.
Besides usual imperative statements, specification statements are
included. Specification statements allow changes of variables to be
described by a predicate. They are abstract in the sense that they are
non-executable. Specification statements may appear in method bodies of
classes, leading to abstract classes.

The motivation for this approach is that abstract classes can be
used for problem-oriented specification in early stages and later
refined to efficient implementations. Various refinement calculi provide
laws for procedural and data refinement, which can be used here for
class refinement. This paper, however, focuses on the semantics of
object-oriented programs and specifications and gives some examples of
abstract and concrete classes.

The semantics is given by a translation of the constructs into the
type system Fsub, an extension of the simple typed lambda-calculus by
subtyping and parametric polymorphism: The state of a program is
represented by a record. A state predicate is a Boolean valued function
from states. Statements, both abstract and concrete, are represented by
predicate transformers, i. e. higher order functions mapping state
predicates (postconditions) to state predicates (preconditions). Objects
are represented by records of statements (the methods) operating on a
record of attributes, where the attributes are hidden by existential
quantification. Classes are understood as templates for the creation of
objects. Classes are represented by records. Inheritance amounts to
record overwriting. Subtyping and parametric polymorphism, e. g.
parameterization of classes by types, are already provided by Fsub. The
advantage of this semantic by translation is that it builds on the
features already provided by Fsub (which are all used). Hence no direct
reference to the model underlying Fsub needs to be made; a summary of
the syntax and rules of Fsub is given.