Using Z, by Jim Woodcock and Jim Davies (PDF Version) (original) (raw)

Using Z

Z is a language for describing patterns of declaration and constraint; it can be used to produce structured, mathematical descriptions. It was developed through application to the specification and design of large, complex software systems. It is well-suited to the description of system or component state, and of transactions upon that state.

This book introduces the mathematical language of Z: logic, sets, relations, and schemas. It introduces also a theory of refinement: a set of rules that can be used to prove that two different designs are consistent in terms of their externally-observable, transactional behaviour.

To obtain an electronic version, click here.

A printed version can be ordered from Pearson's web site.

Jim Woodcock is Professor of Software Engineering at the University of York. Jim Davies is Professor of Software Engineering at the University of Oxford.

The Software Engineering Programme at the University of Oxford offers week-long short courses in software specification and design, using Z and other languages: as individual courses, or as part of a flexible, professional (part-time) masters'.