Hint

Swipe to navigate through the chapters of this book

2016 | OriginalPaper | Chapter

19. Z Formal Specification Language

Author: Gerard O’Regan

Publisher: Springer International Publishing

Published in: Guide to Discrete Mathematics

» Get access to the full version

Abstract

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:

Computer Science Explorer

Purchase now

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.

Title

Z Formal Specification Language

Book

Guide to Discrete Mathematics

Print ISBN: 978-3-319-44560-1

Electronic ISBN: 978-3-319-44561-8

https://doi.org/10.1007/978-3-319-44561-8

DOI

https://doi.org/10.1007/978-3-319-44561-8_19

Author:

Gerard O’Regan

Publisher

Springer International Publishing

Sequence number

Chapter number

Chapter 19