The Z Notation

  • V. S. Alagar
  • K. Periyasamy
Part of the Texts in Computer Science book series (TCS)


The Z notation (pronounced as zed, named after the German mathematician Ernst Zermelo) originated at the Oxford University Computing Laboratory, UK and has evolved over the last decade into a conceptually clear and mathematically well-defined specification language. The mathematical bases for Z notation are ZF set theory and the classical two-valued predicate logic. An interesting feature of the Z specification language is the schema notation. Using schemas, one can develop modular specifications in Z and compose them using schema calculus.


State Space Operation Schema Proof Obligation Existential Quantifier Composite Type 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Alagar VS, Periyasamy K (1996) Real-time object-Z: a language for the specification and design of real-time reactive systems. Technical report, Department of Computer Science, Concordia University, Montreal, Quebec, Canada, June 1996 Google Scholar
  2. 2.
    Baumann P, Lermer K (1995) A framework for the specification of reactive and concurrent systems in Z. In: Proceedings of the fifteenth conference on foundations of software technology and theoretical computer science. Lecture notes in computer science, vol 1026. Springer, Berlin, pp 62–79 CrossRefGoogle Scholar
  3. 3.
    Carrido JM (1995) Specification of real-time systems with extensions to object-Z. In: Proceedings of technology of object-oriented languages and systems (TOOLS), Santa Barbara, CA, pp 167–179 Google Scholar
  4. 4.
    Coombes AC, McDermid JA (1992) Specifying temporal requirements for distributed real-time systems in Z. Technical report YCS176, Computer Science Department, University of York, Heslington, York, UK Google Scholar
  5. 5.
    Duke R, Rose G, Smith G (1995) Object-Z: a specification language for the description of standards. Comput Stand Interfaces 17:511–533 CrossRefGoogle Scholar
  6. 6.
    Hayes IJ (ed) (1987) Specification case studies. Series in computer science. Prentice Hall International, Englewood Cliffs Google Scholar
  7. 7.
    Mahony BP, Hayes IJ (1992) A case-study in timed refinement: a mine pump. IEEE Trans Softw Eng 18(9):817–826 CrossRefGoogle Scholar
  8. 8.
    Meira SL, Cavalcanti ALC (1992) The MooZ specification language. Technical report, Departamento de Informática, Universidade Federal de Pernambuco, Recife—PE, Brasil Google Scholar
  9. 9.
    Morgan C, Vickers T (eds) (1994) On the refinement calculus. Springer, Berlin Google Scholar
  10. 10.
    Potter B, Sinclair J, Till D (1991) An introduction to formal specification and Z. Series in computer science. Prentice Hall International, Englewood Cliffs MATHGoogle Scholar
  11. 11.
    Spivey JM (1992) The fuzz reference manual. JM Spivey Computing Science Consultancy, Oxford OX44 9AN, UK Google Scholar
  12. 12.
    Spivey JM (1992) The Z notation—a reference manual, 2nd edn. Series in computer science. Prentice Hall International, Englewood Cliffs Google Scholar
  13. 13.
    Stepney S, Barden R, Cooper D (eds) (1992) Object-orientation in Z. Workshops in Computing Series. Springer, Berlin Google Scholar
  14. 14.
    Woodcock JCP, Davies J (1996) Using Z: specification, refinement and proof. Series in computer science. Prentice Hall International, Englewood Cliffs MATHGoogle Scholar
  15. 15.
    Wordsworth JB (1992) Software development with Z. Addison-Wesley, Reading Google Scholar
  16. 16.
    The Z Notation, ISO/IEC JTC 1/SC22 CD 13568, September 1995 Google Scholar

Copyright information

© Springer-Verlag London Limited 2011

Authors and Affiliations

  1. 1.Dept. Computer Science and Software Eng.Concordia UniversityMontrealCanada
  2. 2.Computer Science DepartmentUniversity of Wisconsin-La CrosseLa CrosseUSA

Personalised recommendations