![[Z in Practice]](zip2.jpg "[Z in Practice]")
Rosalind
Barden, Susan Stepney, and David Cooper.
There are many books available that provide an introduction to Z and its underlying mathematics. There are also a number of short industrial courses and higher education modules that teach students about the basic mathematical ideas of Z. What is missing is a book aimed at people who have understood the basics of the language and now wish to become users of Z. This book does just that.
Z users may be those who have to write a specification, or they may be 'advanced' readers who need to work from Z specifications, such as reviewers, evaluators, assessors, designers, and programmers.
This book contains plenty of examples of using Z. The examples chosen reflect the fact that not everyone who uses Z specifications has a computer science background. While we address some typical computer science problems we also examine some everyday areas such as games. Our aim is to present example problems that are readily understood.
Many published case studies present solutions to problems without indicating why that particular approach has been taken. Throughout the specifications in this book we have woven commentary on the techniques of Z specification that we are using. These are collected together in a glossary which allows the interested reader to follow links into the case studies to see the techniques in the context of problem solving. These glossary entries vary in complexity, and many are based on our experience of the questions that people often ask on industrial short courses.
The majority of the book is technical, although the early chapters address the more managerial issues of using Z within an organisation. These will be of interest to team leaders who are managing groups of Z specifiers as well as to technical readers.
The typical technical reader will have studied Z to some extent, perhaps by having attended a short industrial course or an introductory higher education course, or by having read an introductory text on Z. The material should also be suitable for people who are familiar with other model-oriented formal specification languages who do not need an introduction to the mathematics involved but want a description of how Z specifications are written.
Although this book contains a glossary and a notation guide it is not a reference manual for the notation. It does not introduce the basic mathematics. It is a practical book of helpful hints and explanations about using Z given in the context of problem solving and specifications.
There are different kinds of text in this book
We use a stylistic convention to distinguish these kinds of text. The accompanying text is interleaved with the Z in the usual manner. The notes are set in a smaller typeface with an indented key identifying phrase, thus
- key phrase
A pedagogical note explaining why the given approach was taken, or why an apparently better approach was not taken, or explaining a more unusual use of the notation.
Appendix B is a comprehensive glossary and cross reference, which should help with finding the information given in these notes. It consists of an alphabetical list of key phrases. Each section consists of a short definition of its key phrase, and list of references to the pages where that phrase occurs, accompanied by a short description of its context. The glossary entry corresponding to the above note would appear as
key phrase
A key phrase is used in each pedagogical note to indicate the content of the note and as a cross reference entry in the glossary. The cross reference entry includes a note of the section in which the glossary reference appears, provided as an aide-mémoire for anyone who knows they have seen the point illustrated somewhere .page xiv: Preface: explanation of glossary structure
Towards the end of the glossary we collect together various discussion points that appear throughout the text. Finally, a list of symbols and their names appears at the end of the glossary.
We have used the definitions and mathematical toolkit of [Spivey 1992] , the de facto standard for Z. In this book it is referred to as the sample toolkit . At the time of writing, a Z standard is being prepared for submission to the British Standards Institute (BSI) and the International Standards Organisation (ISO) [Brien & Nicholls 1992] . The glossary includes some notes of anticipated changes.
This book need not be read in a linear order. As indicated above various readers may find different sections relevant. Below we give an outline of what appears in each chapter to enable readers to select those which are appropriate.
In Part I (Chapters 1--7) we describe various methods that can be used in conjunction with the Z notation for specifying a variety of systems. Chapter 1 sets the scene, giving advice for newcomers to Z, managers, project leaders and specifiers, including some of the management issues involved in using Z on a project. In Chapter 2 we discuss the components necessary in any method: structure, process and fluency. Chapter 3 explains the Established Strategy for writing Z specifications in a 'state and operations' style. An alternative method used for writing security specifications is described in Chapter 4. An overview of other approaches that can be used with Z is given in Chapter 5. In Chapter 6 we discuss ways of checking that a specification is 'correct'. Chapter 7 suggests questions to consider when putting together an appropriate method for using Z.
In Part II (Chapters 8--13) we present five case studies. Our aim is to show Z being used to specify realistic problems. Each case study concentrates on illustrating particular aspects of Z. First in Chapter 8 we describe our 'house style' for the specifications in the book.
In Chapter 9 we examine the familiar computer science problem of counting words within a document and producing frequency tables. We start with a simplistic specification which takes a 'lateral' view of what a word might be. We then specify the solution in increasingly complex ways, finishing with an implementation-oriented specification based on Unix. Our aim is to show that a problem can be solved at varying levels of abstraction. We wish to encourage you to pick the most abstract specification appropriate for your needs.
In Chapter 10 we illustrate how the schema calculus, in particular schema conjunction and disjunction, can be used to structure a specification, here of a space flight company. (Further use of schemas is covered in Chapter 23.)
Structuring specifications is looked at in a different way in Chapter 11. We use Entity Relationship Diagrams to break down the problem and guide the structure of the specification of a video hire shop. We concentrate on operations such as checking that a borrower is old enough to hire a given film, rather than on the mechanics of borrowing and returning videos. Such operations have been described elsewhere in specifications of book-lending libraries, including [King & Sörensen 1989] , [Diller 1990] , [Potter et al 1991] and [Wordsworth 1992] .
The techniques of precondition calculation and promotion are used in Chapter 12. The way in which preconditions are calculated is described in some detail, whereas the use of promotion is just illustrated. For a full explanation of promotion you should read Chapter 19.
Chapter 13 provides solutions to the Tower of Hanoi problem. The main aim of this chapter is to illustrate the process of refinement. As this book is primarily about specification, we do not show a full transformation towards code. Rather we show how a more concrete solution refines the abstract view and give the required proofs.
This part contains the largest specifications in the book. Subsequent chapters look at smaller problems to illustrate various useful points.
In Part III (Chapters 14--19) we look at some common Z styles that have been found to be useful, and that you can use or adapt for your own purposes.
Abstraction is a desirable property of specifications. A specification that is too concrete includes unnecessary details that makes it difficult to read, and may also include premature design or implementation decisions that are better left until later. An abstract specification, on the other hand, includes only the essentials of the problem eschewing clutter and deferring design decisions to a later, more appropriate, time. Abstraction is notoriously difficult to define, so we have side-stepped the problem by providing some examples of abstraction in Chapter 14, pointing out where the temptations to be more concrete have been avoided.
Next we discuss various modelling choices. In Chapter 15 we present the same small specification using two different models (using sets and using functions) and discuss their advantages and disadvantages. Chapter 16 contrasts various styles of defining sets.
In Z sequences are functions, which are relations, which are sets. Chapter 17 describes how this means that specifications can sometimes be simplified by using set operations where, at first sight, they might not seem applicable.
If examples are always presented using one particular style there is the danger that such a style might be assumed to be the only one possible. The treatment of errors is one such case since the Established Strategy of disjoining error handling with the 'correct' operation is the one presented most often. In Chapter 18 we contrast this approach with an alternative way of describing error cases.
In Chapter 19 we explain the technique of promotion, a style for structuring specifications that can lead to clear and compact descriptions.
In Part IV (Chapters 20--26) we look at some of the less common aspects of Z. Our aim is to explain the use of those symbols that are often ignored or given only a glance in introductory texts. We illustrate some uses for them.
Free types often cause difficulties, especially in their recursive form. Chapter 20 illustrates the various forms of free types and their uses. We end on a note of caution with an example of a tree specification. At first it appears that this is the classical application of a recursive free type, but a different model proves to be more appropriate for specifying the required operations.
Bags are an underused part of Z, but at times they are useful. In Chapter 21 we illustrate some cases where bags are applicable.
Next, in Chapter 22, we look at axiomatic descriptions. Not every specification uses schemas and the example of the four function calculator contrasts a specification using schemas with one that does not. This chapter also includes a discussion of the different ways of under-specifying.
Having shown how sometimes schemas are not necessary, in Chapter 23 we move on to examine the many uses of schemas that are possible. This extends Chapter 10 by illustrating other parts of the schema calculus, the use of schemas as predicates, and the way in which one can quantify over schemas.
Chapter 24 provides explanation of other parts of the notation. Here we look at restrictions on relations, generic definitions and the usefulness of disjoint and partition . We then go on to explain θ and μ, which often cause confusion.
Chapter 25 has a discussion on toolkits, and we provide a real number toolkit as an illustration of how toolkits may be devised. In Chapter 26 we look back over the book and ahead to the future of Z.
Finally, Part V contains a variety of appendices. Appendix A describes the extensions to the sample mathematical toolkit that we have used in the main text of the book. Appendix B is a glossary as described earlier. Appendix C contains a list of all the references mentioned in the book.
Many people have contributed in a number of ways to this book, commenting on various drafts, suggesting examples for specification, and discussing approaches to specification. Our thanks to you all.
In particular, the file system examples in sections 16.3 and 20.6 are based on the work of Trevor King, and we are grateful to him for permission to use them. The example in section 24.2 is used with the permission of Ian Stewart. The example used in Chapter 11 was suggested by Andy Gravell, and that of Chapter 13 is a problem set by Neville Dean to his students.
We would also like to thank the following people who helped in other ways: Jardine Barrington-Cook, Tony Boswell, Stephen Brien, Neville Dean, Tim Denvir, Andy Gravell, Hans-Martin Hörcher, Iain Houston, Debi Kearney, Haim Kilov, Steve King, Trevor King, Kevin Lano, John McDermid, Fiona Polack, Jo Primrose, Julian Rose, Paul Smith, Roger Stokes, Sam Valentine, John Wordsworth and Nick Youd.
Our thanks also to Aldus (for IntelliDraw), Donald Knuth (for TeX), Leslie Lamport (for LaTeX), Ed Sznyter of LaTeX-help@stanford.edu (for help with LaTeX macros), Mike Spivey (for fuzz), and Paul King (for oz.sty), without whom this book would have looked very different.
The quadrilaterals example of sections 23.6 and 24.6.4 is based on the work in [Stepney et al 1992] . Some of the other examples have been developed from those presented in Logica's course on Z specification --- we are grateful to all those participants of the courses who have helped to make these examples more interesting and, above all, less error prone.
Much of this work was carried out as part of the ZIP project, which was an IED initiative, project number IED4/1/1639. The part-funding by the United Kingdom's Department of Trade and Industry is gratefully acknowledged.
Finally, thanks are due to our employers, Logica UK Limited , for providing the backing that allowed us to produce the book.
Rosalind Barden
Susan Stepney
David Cooper
Cambridge, England
August 1994