page 2  (40 pages)
to previous section1
3to next section

Refinement of Concurrent Object Oriented

Programs

Paulo Borba? and Joseph A. Gogueny

Programming Research Group

Oxford University Computing Laboratory

November 1995

Abstract

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.

1 Introduction

FOOPS is a concurrent object oriented specification language having an executable subset [Goguen and Meseguer, 1987, Rapanotti and Socorro, 1992]. It includes a functional language derived from OBJ [Goguen and Winkler, 1988], which is a first order, purely functional language providing an algebraic style for the specification, rapid prototyping, and implementation of abstract data types. OBJ also supports

?Supported by CAPES, Brazil, Grant 2184-91-8, and the CEC under ESPRIT-2 BRA Working Group 6071, IS-CORE (Information Systems COrrectness and REusability). Electronic mail: phmb@di.ufpe.br.
ySupported in part by the Science and Engineering Research Council, the CEC under ESPRIT- 2 BRA Working Groups 6071, IS-CORE (Information Systems COrrectness and REusability) and 6112, COMPASS (COMPrehensive Algebraic Approach to System Specification and development), Fujitsu Laboratories Limited, and a contract under the management of the Information Technology Promotion Agency (IPA), Japan, as part of the Industrial Science and Technology Frontier Program New Models for Software Architectures," sponsored by NEDO (New Energy and Industrial Technology Development Organization). Electronic mail: Joseph.Goguen@prg.oxford.ac.uk.