PLS Lab

Z notation

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.

Types

There is a type checker for Z, called fuzz.

Standardization

Since 2002, Z has been an ISO standard (ISO/IEC 13568:2002).

Other trivia

The Oxford University Computer Laboratory was awarded the Queen's Award for Technological Achievement in 1992 for the development of Z, jointly with IBM.

See also

References

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. 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},
}