Rosalind Barden, Susan Stepney, and David Cooper.
Z in Practice .

BCS Practitioner Series. Prentice-Hall, 1994.

ISBN 0-13-124934-7

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:

  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
    1. House Style
    2. A Word Counting Utility
    3. Roles in Space
    4. Structuring a Video Shop
    5. Promoting Snakes and Ladders
    6. Refining the Tower of Hanoi
  3. Style and Tactics
    1. Be Abstract
    2. Sets or Functions?
    3. Sets, Quantifiers, or Toolkit?
    4. Sequences are Functions are Relations are Sets
    5. Error Handling Styles
    6. Promotion
  4. Z Notation Details
    1. Using Free Types
    2. Using Bags
    3. A Four Function Calculator
    4. Making Schemas Work for You
    5. Exploiting the Power of the Language
    6. A Real Number Toolkit
    7. And Finally...
  5. Appendices
    1. Extension to the Sample Toolkit
    2. Glossary and Cross References
    3. Bibliography
  author = "Rosalind Barden and Susan Stepney and David Cooper",
  title = "Z in Practice",
  publisher = "Prentice-Hall",
  series = "BCS Practitioner Series",
  year = 1994