Swipe to navigate through the chapters of this book
This chapter presents the Z specification language, which is one of the most widely used formal methods. 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. 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.
Please log in to get access to your license.
Dont have a licence yet? Then find out more about our products and how to get one now:
Stepwise 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.
This project claimed a 9% increase in productivity attributed to the use of formal methods.
go back to reference A. Diller, Z. An Introduction to Formal Methods (John Wiley and Sons, England, 1990) A. Diller, Z. An Introduction to Formal Methods (John Wiley and Sons, England, 1990)
go back to reference G. O’Regan, Guide to Discrete Mathematics (Springer, 2016) G. O’Regan, Guide to Discrete Mathematics (Springer, 2016)
- Z Formal Specification Language
- Copyright Year
- Springer International Publishing