The formal specification notation Z (pronounced "zed"), useful for describing computer-based systems, is based on Zermelo-Fraenkel set theory and first order predicate logic. It has been developed by the Programming Research Group (PRG) at the Oxford University Computing Laboratory (OUCL) and elsewhere since the late 1970s, inspired by Jean-Raymond Abrial↑'s seminal work. Z is now defined by an ISO standard and is public domain. "" indicates new entries. See information on:
- An announcement concerning Z and WWW
- The Z archive
- Frequently Asked Questions
- Mailing lists and newsgroups
- Meetings including ZUM
- Tool support (organized alphabetically)
- The related method VDM
- The Z User Group
- Z in French
- Z Bibliography
- Extensions in HTML for Z
- Z standardization
- TCOZ (Timed Communicating Object Z)
- The B-Method
- Other information
Please contact Jonathan Bowen if you know of relevant online information not included here. Use the comp.specification.z newsgroup (submissions also possible via email on [mailto: firstname.lastname@example.org email@example.com]) for general Z-related queries.
- 1 Frequently Asked Questions (Z FAQ)
- 2 The Z archive
- 3 Mailing lists and newsgroups
- 4 Publications
- 5 Z standardization
- 6 Meetings
- 7 Courses
- 8 Tool support
- 9 Z and VDM
- 10 Other information
- 11 External links
Frequently Asked Questions (Z FAQ)
If you wish to discover more about Z, a Frequently Asked Questions document (with answers) is available in plain text, which is periodically updated, in a hypertext version (see also here), and a nicely formatted (but rather outdated — 1998) PDF version for the Z User Meeting proceedings. Also available (but out of date) in Japanese and mirrored in Germany and in France. See also another Z entry.
Z is a formal (i.e., mathematical) specification notation used by industry (especially in high-integrity systems) as part of the software (and hardware) development process in both Europe and the US. It has undergone international standardization under ISO/IEC JTC1/2 WG19 on formal specification languages. The use of Z resulted in a UK Queen's Award for Technological Achievement in 1992 for its use in the IBM CICS project and contributed towards one in 1990 for its use to specify the IEEE Standard for Binary Floating-Point Arithmetic (see Technical Monograph PRG-58).
The Z archive
An electronic archive of Z-related files is still available via anonymous FTP with associated index and README files. The archive was transferred to the ZUG website in November 2002. However, some files may still be useful. A Z bibliography is available. Older versions are available in BibTeX database and compressed PostScript format.
Mailing lists and newsgroups
To subscribe to Z FORUM, an electronic mailing list on the Z notation, send e-mail to firstname.lastname@example.org with "subscribe" in the body (not the subject line) of the message or use the online Z FORUM request form. Send a message of "unsubscribe" to leave the list. To submit articles for Z FORUM, you can send e-mail to email@example.com. Articles are sent out as they arrive to ensure timeliness. This mailing list is gatewayed to the comp.specification.z USENETnewsgroup. You are advised to read articles via the newsgroup if you have access to it. The mailing list is maintained as a service to those without easy access to news. Older messages are archived under anonymous FTP under the files zforum*. See also FAQ (Frequently Asked Questions) message (alternatively available from Newsville) derived from the plain text FAQ message sent out monthly on the newsgroup and mailing list.
You can access comp.specification.z articles via the Web from Google Groups. See also comp.specification.z Frequently Mentioned Resources and other comp.specification.* newsgroup resources from People Helping One Another Know Stuff (PHOAKS), which gives a count of and link to URLs mentioned in newsgroup articles.
A postal mailing list is also maintained, mainly for information about meetings. If you wish to join, please email Amanda Kingscote on firstname.lastname@example.org.
A specialist electronic mailing for discussion of the SAZ method, a combination of the structured method SSADM and Z existed for a while but is now closed.
A searchable Z bibliography is available. The Z archive contains an older [Z BibTeX bibliography] of Z-related publications in BibTeX↑ format, which is available as a Technical Report entitled Select Z Bibliography. The bibliography is also available in a standardized format.
If you would like information about publications produced at the PRG such as Technical Monographs (in particular, see PRG-46, PRG-47, PRG-48, PRG-49, PRG-50, PRG-58, PRG-60, PRG-61, PRG-62, PRG-63, PRG-68, PRG-74, PRG-81, PRG-101, PRG-103, PRG-107 which relate to Z) and Technical Reports (including many relating to Z), please contact the OUCL librarian.
A survey on the Assessment of the Use of Formal Methods includes real examples of Z in industrial use.
The following online WWW pages associated with Z books are available:
- Formal Specification and Documentation using Z: A Case Study Approach, Jonathan Bowen. International Thomson Computer Press, International Thomson Publishing, 1996.
- Using Z: Specification, Refinement and Proof, Jim Davies and Jim Woodcock↑. Prentice Hall International Series in Computer Science, 1996. See information from the publisher.
- The Way of Z: Practical Programming with Formal Methods, Jonathan Jacky. Cambridge University Press, 1997.
- The Z Notation: A Reference Manual, 2nd edition, Mike Spivey. Prentice Hall International Series in Computer Science, 1992. (De facto standard reference book for Z.)
See also links to formal methods publications in general.
An international Z standardization effort was completed in 2002. The ISO/IEC Z Standard is available as Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics, ISO/IEC 13568:2002, from ISO. A printed copy of Version 1.0 of the Z Base Standard (an early version) is available as PRG Technical Monograph PRG-107. Further developments are still under consideration. For further information, see:
See information on ANSI NCITS/J21 (formerly X3J21) technical committee. See also J21 Technical Committee information from the Accredited Standards Committee NCTIS/J21, National Committee for Information Technology Standards (NCITS), USA, including Z standard scope.
Note that UNICODE character encoding now includes Z symbols. See especially Miscellaneous Mathematical Symbols-A, Miscellaneous Mathematical Symbols-B and Supplemental Mathematical Operators. The Z Standards Panel would like to thank the STIX Project for getting these added to the Unicode Standard.
ZB2002 was held at Grenoble, France, 23–25 January 2002.
ZB2003 was held at Turku, Finland, 4–6 June 2003.
The 9th International Conference of Z Users (ZUM'95), was held at the University of Limerick, Limerick, Ireland↑, 7–8 September 1995, at the invitation of the Department of Computer Science and Information Systems (CSIS). There was a Limericks Competition associated with the meeting for aspiring poets!
An announcement of the availability of this and other formal methods WWW pages was made at the meeting. It was noted that the availability of coffee can be checked at Cambridge↑. At the time, this received around 1,000 accesses a day. The formal methods pages at Oxford↑ only receive around 400 accesses per day!
Previous Z User Meeting proceedings (e.g., ZUM'92) have been published by Springer-Verlag in their Workshops in Computing series since the 1989 meeting. Early proceedings were published informally by the Oxford University Computing Laboratory and the main parts of the 1987 and 1988 meetings are available online.
See also information on other formal methods meetings.
A Z course is taught at Altran Praxis↑.
Community Z Tools
The Community Z Tools (CZT) project is an open source project providing an integrated toolset to support Z, with some support for Z extensions such as Object-Z, Circus, and TCOZ. These tools are all built using the CZT Java framework for Z tools.
Fastest is a model-based testing tool. The tool receives a Z specification and generates in an almost automatic way, test cases derived from the specification. Currently, it only provides limited functionality for test case refinement into C and Java.
ProofPower is a suite of tools supporting specification and proof in Higher Order Logic (HOL) and in the Z notation. ProofPower has been under ongoing development since 1989. It was originally designed and implemented by International Computers Ltd. to support proofs of specification-to-model correspondence for high-assurance secure systems. It has since played an important role in approaches to specifying and verifying safety-critical systems in work by the Defence and Evaluation Research Agency, now QinetiQ, and others. Since 1997, on-going developments to the product have been undertaken by Lemma 1 Ltd.
Z Word Tools
The Z Word Tools allow Z specifications to be written in Microsoft Word↑. They include a Unicode↑ font for Z symbols and capabilities for editing, typechecking (using fuzz or CZT), indexing and cross-referencing and creation of diagrams showing specification structure. They support large specifications in multiple Word documents. The tools are available from the Z Word Tools Project on SourceForge↑.
A Z animator is planned as part of the CZT project. There are some earlier experimental animators:
- Mathias Mathematics in Animation Suite, including advice on using it to animate Z and references to papers on Suzan (the Surrey Z Animation project).
TrueType↑ Z fonts are available with the Z Word Tools and CZT projects. In addition there is a Zed font for Windows and Macintosh by Richard Jones, Computing Laboratory, University of Kent at Canterbury, UK. Microsoft Word 2007 or later includes the Cambria Math font, which includes all Z symbols.
Other Z tools
- Moby/OZ, a graphical editor to build Z and Object-Z specifications.
- RoZ — Production of formal Z specifications from annotated UML diagrams
- Wizard, a type-checker for Object-Z specifications in LATEX↑.
- Z/EVES is a proof tool based on ZF set theory. Originally available from ORA Canada, its status is now uncertain.
- HOL-Z is an interactive theorem prover for Z based on Isabelle/HOL.
Z and VDM
See also a comparison of Z, VDM and the B-Method.
Information on object-oriented extensions of Z, such as Object-Z, Z++ and ZEST (Z Extended with STructuring) is available elsewhere. See the book Object Orientation in Z, including further hyperlinks and a bibliography.
- Z specification language↑ entry in the Wikipedia free online encyclopedia.
- Formal methods and Z information by Susan Stepney.
- B-Method for formal software development.
- Choosing between Z and PVS and other formal methods humour.
- Z language, Z books and Set Theory links from the Google Directory.
- Zed Soup — (A)nna to (Z)ed Recipes for Formal Specifications, by Jack Beidler.
For some entirely different and unrelated "Z" links, if you are tired of the "real" thing, see:
- Mega-Z FAQ.
- Z-editor for modifying web pages.
- ZEE-ART, combining art and mathematics.
- zed mobile phone services!
- Zed Books, publishers of academic books.
- Zed simple fast Unix editor for "vi" haters!
- Z-Bend Pliers — perfect Z bends every time! See also Precision Z-Bend Pliers — the tool for making better Z-bends!
- Z Car Home Page — see also Z Cars 1960s British TV series.
Comments, corrections and new information are gratefully received.
Last updated by Jonathan Bowen, 30 March 2012.