The Z notation is a language for formally specifying computer systems.
It was developed in the 1970s and (mostly) in the 1980s, primarily by Jean-Raymond Abrial.
It was used to specify IBM's Customer Information Control System (CICS), an on-line transaction processing system used at the time by major financial and retail organisations. A report on this experience - a positive assessment! - is available in [Collins et al. 1987].
There is a type checker for Z, called fuzz.
Since 2002, Z has been an ISO standard (ISO/IEC 13568:2002).
The Oxford University Computer Laboratory was awarded the Queen's Award for Technological Achievement in 1992 for the development of Z, jointly with IBM.
J. M. Spivey. The Z Notation: A Reference Manual. Prentice Hall International, 1989. (2nd edition 1992 - pdf)
J. M. Spivey. Understanding Z—A Specification Language and its Formal Semantics. Cambridge Tracts in Computer Science 3. Cambridge University Press, 1988. (reprinted 2008)
Mike McMorran and Steve Powell. Z Guide for Beginners. Alfred Waller Limited, 1993.
Jim Woodcock and Jim Davies. Using Z: Specification, Refinement and Proof. Prentice Hall International, 1996.
B.P. Collins, J.E. Nicholls, and I.H. Sorensen. Introducing formal methods: The CICS experience with Z. Technical Report TR12.060, IBM Hursley Laboratory, 12 1987.
A discussion of the history of Z in the UK formal methods community can be found in
The influence of VDL is remarked upon in
Cliff B. Jones and Martyn Thomas. 2022. The Development and Deployment of Formal Methods in the UK. Form. Asp. Comput. 34, 1, Article 6 (March 2022), 21 pages. https://doi.org/10.1145/3522577 [arXiv]
@article{10.1145/3522577,
author = {Jones, Cliff B. and Thomas, Martyn},
title = {The Development and Deployment of Formal Methods in the UK},
year = {2022},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {34},
number = {1},
issn = {0934-5043},
url = {https://doi.org/10.1145/3522577},
doi = {10.1145/3522577},
journal = {Formal Aspects of Computing},
articleno = {6},
numpages = {21},
}