Preface

This collection of papers draws together a variety of approaches for adding object orientation to the Z formal specification language. These papers are not a conference proceedings, but have a slightly more complicated history.

This work has grown and evolved from some work originally done in the ZIP project, under the United Kingdom's Department of Trade and Industry (DTI) IED initiative. ZIP is a three year project which aims to make the use of the Z specification language more widespread. It hopes to achieve this by producing a standard for Z; developing a method for Z ; building tool support for Z; and carrying out research into refinement, proof and concurrency in Z.

The ZIP methods work includes performing a survey of current Z practitioners (reported in [Barden et al. 1992] ); investigating current styles and methods of Z usage; and developing a Z Method handbook (available early in 1993). As part of this work, we carried out a comparative study of the ways in which object orientation has been combined with Z. A summary of that work has been published as [Stepney et al. 1992] .

In the Summer of 1991, the ZOOM workshop was held at Lady Margaret Hall, Oxford, organized and funded by the Z User Group. At this workshop, various parties interested in combining object orientation and Z formal specifications got together. There are no published proceedings, but the discussions are reported in [Carrington 1992] . As part of the material supplied to participants, a copy of the ZIP comparative study was distributed. When proponents of other 'object oriented Z' approaches saw the document, they expressed interest in having their own methods represented.

Consequently, a new document was prepared, structured as a series of 'authored chapters'. This was distributed to participants at the 6th Annual Z User meeting , held at the University of York in December 1991. The new document was well received, and Springer-Verlag agreed to publish a revised version in their 'Workshops in Computing' series. For this version, many chapters have been substantially revised, and a new chapter describing a further approach has been added.

We would like to thank all the authors of the various chapters, without whose enthusiasm and hard work this book would not have been possible. We would also like to thank Anthony Hall, Brian Hepworth, Trevor King and David Pitt for their help. The part funding by the DTI for ZIP (project number IED4/1/1639) is gratefully acknowledged.