Oxford University Computing Lab, Programming Research Group Technical Report TR-18-95

Refinement of Concurrent Object Oriented Programs

by Paulo Borba and Joseph Goguen

November 1995, 39pp

FOOPS is a concurrent object oriented language. Based on FOOPS operational semantics, we introduce a notion of refinement for states of FOOPS systems together with a proof technique for proving refinement. Using this notion, we define refinement of FOOPS (method) expressions and programs. Although we focus on FOOPS, our definition of refinement is independent of this language.

We also illustrate the use of refinement for stepwise formal development of programs in FOOPS. Based on that, we give an overall evaluation of our approach and comment on alternative approaches for the refinement of concurrent object oriented programs, concluding that none of them provide both a general definition of refinement and an effective proof technique such as the one presented here.

This paper is available as a gzipped PostScript file.
To FOOPS homepage
To Systems index page
To Joseph Goguen homepage
Maintained by Joseph Goguen
Last modified 23 February 1999