Abstract
Z is a formal specification language based on Zermelo set theory. It was developed at the Programming Research Group at Oxford University in the early 1980s (Diller, An Introduction to Formal Methods, 1990), and became an ISO standard in 2002. Z specifications are mathematical and employ a classical two-valued logic. The use of mathematics ensures precision and allows inconsistencies and gaps in the specification to be identified. Theorem provers may be employed to demonstrate that the software implementation meets its specification.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Step-wise refinement involves producing a sequence of increasingly more concrete specifications until eventually the executable code is produced. Each refinement step has associated proof obligations to prove that the refinement step is valid.
- 2.
This project claimed a 9 % increase in productivity attributed to the use of formal methods.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2013 Springer-Verlag London
About this chapter
Cite this chapter
O’Regan, G. (2013). Z Formal Specification Language. In: Mathematics in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-4534-9_6
Download citation
DOI: https://doi.org/10.1007/978-1-4471-4534-9_6
Published:
Publisher Name: Springer, London
Print ISBN: 978-1-4471-4533-2
Online ISBN: 978-1-4471-4534-9
eBook Packages: Computer ScienceComputer Science (R0)