Z.: An Introduction to Formal Methods

This book is about the formal specification language Z. It is based on two lecture courses given in the School of Computer Science at the University of Birmingham. Given its origins this book can be used as a textbook for courses on Z and formal methods at first and second year undergraduate level. This book is divided into seven parts. Part 1 contains a single chapter which aims to explain what Z is and why it is a good method for specifying software components. Part 2 is a tutorial introduction to Z which covers the basic mathematicl toolkit of Z and the fundamental ideas of the schema calculus and part 3 looks at methods of reasoning. Part 4 contains four specification case studies: two small ones and two fairly large ones. The two small ones are of the bill of materials problem and of a simple route planner. The two large case studies are of a display-orientated text-editor based on Sufrin's specification and of Wing's library problem. Part 5 looks at how a Z specification can be animated using a high level modern functional programming language and Prolog. Part 6 is a reference manual of all the most frequently used Z notations and Part 7 consists of two appendices as well as an annotated bibliography which contains many pointers into the ever-increasing literature on Z.