An Object-Oriented
Refinement Calculus
with Modular Reasoning

A dissertation submitted to the
University of New South Wales,
Kensington, Australia

by

Mark Utting

in fulfillment of the requirements for the degree of

Doctor of Philosophy.

April 8, 1992
(plus errata, October 1992)

Abstract

In this thesis, the refinement calculus is extended to support a variety of object-oriented programming styles. The late binding of procedure calls in object-oriented languages is modelled by defining an object-oriented system to be a function from procedure names and argument values to the procedures that are invoked by late binding. The first model allows multiple dispatch late binding, in the style of CLOS. This model is then specialised to the single dispatch case, giving a model that associates types with objects, which is similar to existing class based object-oriented languages.

Both models are then restricted so that they support modular reasoning. The concept of modular reasoning has been defined informally in the literature, both for non-object-oriented systems and for object-oriented systems. This thesis gives the first formal definition of modular reasoning for object-oriented languages. Intuitively, the definition seems to capture the minimum possible requirements necessary to support modular reasoning. For simplicity, the definition only allows data refinement between the implementation and specification of an object, not between types and subtypes. The removal of this restriction is discussed in the section on further work.

The definition of modular reasoning allows programs to make arbitrary observations about objects, such as testing the type of an object. In contrast, most existing formal methods for object-oriented programming assume that a subtype should be a transparent replacement of its supertypes, so do not allow programs to test the types of objects.

Other topics covered include the incremental construction of types from other types and a way of reasoning about the aliasing of objects, based on the collections of Euclid. The use of collections to handle aliasing is convenient because it is modular. That is, an object can encapsulate a collection and thus hide all aliasing from programs that use the object.


The full thesis is available as postscript (320K).

Chapter four, which contains the main technical results, was published as:

@InProceedings{utting:mod-reas-in-oo-refcalc,
  author =    "Mark Utting and Ken Robinson",
  title =     "Modular Reasoning in an Object-Oriented Refinement Calculus",
  booktitle = "Mathematics of Program Construction.  Second International
               Conference, Oxford, U.K., June/July 1992",
  year =      1993,
  editor =    "R. S. Bird and C. C. Morgan and J. C. P. Woodcock",
  pages =     "344-367",
  publisher = "Springer-Verlag",
  note =      "LNCS~669",
  annote =    "Defines a multiple dispatch object-oriented language
               and shows various ways of reasoning about programs in
               a modular fashion."
 }

marku@cs.waikato.ac.nz
Last modified: Thu Mar 13 12:05:15 NZDT 1997