Swipe to navigate through the chapters of this book
Chapter 19 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 this content
To get access to this content you need the following product:
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.
This project claimed a 9 % increase in productivity attributed to the use of formal methods.
Z. An Introduction to Formal Methods. Antoni Diller. John Wiley and Sons. England. 1990.
- Z Formal Specification Language
- Springer International Publishing
- Sequence number
- Chapter number
- Chapter 19