This book describes various methods for developing Z specifications, and explains some advanced Z techniques. It is aimed at people who already understand the basics of Z and now wish to become users of it. It includes five case studies and many smaller examples of using Z, illustrating different features of the language. It also contains a comprehensive glossary with links to examples in the main text that illustrate the definitions in use.

ZIP was a collaborative UK DTI-IED project set up to improve the take-up and use of Z in industry. The partners were BAe, BP, IBM, Logica, Oxford PRG, Praxis, and RAL. This book grew out of some of the methods work done on the ZIP project.

Recommended text for the MSc in Advanced Computing 1995/96 -- University of Bristol Department of Computer Science

Table of Contents:

• Preface

1. Using Z
   1. Welcome to Z Newcomers
   2. Structure, Process, Fluency
   3. The Established Strategy
   4. Security Properties
   5. Other Approaches to Z Specification
   6. Validation
   7. Putting Together Your Model
2. Case Studies
   8. House Style
   9. A Word Counting Utility
   10. Roles in Space
   11. Structuring a Video Shop
   12. Promoting Snakes and Ladders
   13. Refining the Tower of Hanoi
3. Style and Tactics
   14. Be Abstract
   15. Sets or Functions?
   16. Sets, Quantifiers, or Toolkit?
   17. Sequences are Functions are Relations are Sets
   18. Error Handling Styles
   19. Promotion
4. Z Notation Details
   20. Using Free Types
   21. Using Bags
   22. A Four Function Calculator
   23. Making Schemas Work for You
   24. Exploiting the Power of the Language
   25. A Real Number Toolkit
   26. And Finally...
5. Appendices
   1. Extension to the Sample Toolkit
   2. Glossary and Cross References
   3. Bibliography

@book(SS-ZIP,
  author = "Rosalind Barden and Susan Stepney and David Cooper",
  title = "Z in Practice",
  publisher = "Prentice-Hall",
  series = "BCS Practitioner Series",
  year = 1994
)