The Z notation

Last conference: ZUM'98, Berlin, Germany, 24-26 September 1998
Last meeting: ZUG meeting at FM'99, Toulouse, France, 20-24 September 1999
Last conference:

ZB2000, York, UK, 29 August - 2 September 2000.

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. See information on:

Interactive forms (if supported by your WWW client):

Request concerning ZFORUM mailing list
Comments

Please mail J.P.Bowen@reading.ac.uk if you know of relevant on-line information not included here. Use the comp.specification.z newsgroup (submissions also possible via email on zforum@comlab.ox.ac.uk) for general Z-related queries.

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, and a nicely formatted PostScript version for the Z User Meeting proceedings. Also available in Japanese and mirrored in France. See also another Z entry and a dictionary definition of Z in the on-line software engineering glossary.

Z is now used by industry as part of the software (and hardware) development process in both Europe and the US. It is undergoing international standardization under ISO/IEC JTC1/SC22 WG19 on formal specification languages through the UK. The use of Z has 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 available via anonymous FTP with associated index and README files. The archive is mirrored at Imperial College and Queen Mary and Westfield College, London. A searchable Z Bibliography is available. Older versions are available in BibTeX database and compressed PostScript format.

In addition there are many OUCL Technical Monographs and Technical Reports on Z.

Mailing lists and newsgroups

To subscribe to Z FORUM, an electronic mailing list on the Z notation, send e-mail to zforum-request@comlab.ox.ac.uk with "subscribe" in the body (not the subject line) of the message or use the on-line 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 zforum@comlab.ox.ac.uk. Articles are sent out as they arrive to ensure timeliness. This mailing list is gatewayed to the comp.specification.z USENET newsgroup You are requested to read articles via the newsgroup if you have access to it. The mailing list is being maintained as a service to those without access to news. Older messages are archived under anonymous FTP under the files zforum*. See also FAQ (Frequently Asked Questions) message (alternatively available in Oxford) derived from the plain text FAQ message sent out monthly on the newsgroup and mailing list.

You can access comp.specification.z articles, search for comp.specification.z references and browse message sent within the last month or last week via the Web from Dejanews. Comp.specification.z is also accessible from Lycos remarQ. 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 ark@praxis-cs.co.uk.

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.

Other related newsgroups of interest are comp.specification.misc, comp.specification.*, comp.software-eng and the moderated comp.risks Z User Meetings are announced in the newsgroup news.announce.conferences as well.

Publications

An on-line list of Z books (see also here and here) is also available from Amazon.com Books. See also Amazon.co.uk UK site.

A searchable Z bibliography is available. The Z archive contains an older BibTeX bibliography of Z-related publications which is available as a Technical Report entitled Select Z Bibliography. The bibliography is also available in a standardized format. A regularly updated list of books is also available. The FACS Europe newsletter includes Z-related material.

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.

A 2-page Z Glossary (in PostScript format) is available on-line.

The following on-line 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.)

A Z Special Issue of the Information and Software Technology journal. (vol. 37, no. 5-6, May/June 1995) is available.

See also links to formal methods publications in general.

Z standardization

An international Z standardization effort is underway, including on-line copies of Z standards drafts and proposals. A printed copy of Version 1.0 of the Z Base Standard is available as PRG Technical Monograph PRG-107. For further information on the Z Base Standard, please contact John Nicholls or Andrew Martin. New FTP information concerning the standard is installed as it becomes available. For recent developments, see:

Z standards documents from Rob Arthan
Z standards documents from Andrew Martin
Z standards from Ian Toyn

See information on previous funding, 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.

Meetings

The Z User Group (ZUG) organizes the Z User Meeting series, now known as the International Conference of Z Users.

The last ZUG meeting was held as part of FM'99: World Congress on Formal Methods, Toulouse, France, 20-24 September 1999.

The next main conference, ZB2000, will be held in conjunction with the B User Group, York, UK, 29 August - 2 September 2000.

The 11th International Conference of Z Users (ZUM'98) was be held in Berlin, Germany, 24-26 September 1998.

The 10th International Conference of Z Users (ZUM'97) took place at The University of Reading on the outskirts of Reading, 3-4 April 1997.

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! See information on the proceedings.

ZUM'94 was held on 29-30 June 1994 at St. John's College, Cambridge.

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 1000 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 on-line.

Information on these and other related meetings is available elsewhere. See also a list of formal methods events and information on other formal methods meetings.

Courses

There are various courses at OUCL which include the teaching of Z. There are a number of external courses offered by OUCL. Contact Jim Woodcock for details. Logica offer a 5 day course on Formal Software Specification using Z. See also the Z FAQ message for further information on courses.

Tool support

Mike Spivey's original style file for writing Z documents using the L^ATEX document preparation system (see also the MiKTeX system for Windows users) is available as zed.sty together with a guide in L^ATEX source or compressed PostScript format. If you are a L^ATEX2e user, the latest oz.sty below is recommended instead.

Other Z styles files (and associated type-checkers) include:

FuZZ Z type-checker available commercially, together with an associated fuzz.sty L^ATEX style file which has better fonts for the more esoteric Z symbols. Contact Mike Spivey about this and/or see the order form. The type-checker runs on Sun workstation, PC and VAX/VMS equipment. Free version for Linux and other Unix systems (including source).
mz.sty has been developed by Marc Mengel mengel@fnal.gov to work with L^ATEX2e and multiple fonts. It is compatable with zed.sty and the ZTC type-checker L^ATEX-Zed input format. It requires the latexsyms.sty style file.
Object-Z LaTeX Macros for L^ATEX 2.09 (oz.sty) and 2e (oz2e.sty), including documentation.
zed-cm.sty has been further developed to work with L^ATEX2e, together with some documentation files.

The following Z tools are also available:

Alcoa: Alloy Constraint Analyzer, based on a Z-like language for object models.
CADiZ provides support for Z using troff and L^ATEX on Unix systems and Microsoft Word on PCs from York Software Engineering Ltd. A CADiZ home page and FTP site including an overview paper are also available.
Cogito - methodology and toolset for the formal development of software. Uses the Sum specification and development language, based on the Z notation. See also Ergo theoroem prover.
Formaliser Z type-checker, ZEST type-checker, and other formal methods tools and services from Logica.
See also Rose Formaliser Link (Z and UML) and ZView Browser (a free downloadable utility which runs under Windows 95 or Windows NT) for Formaliser/ZEST users. From Headway Software.
HOL mechanical theorem proving system based on Higher-Order Logic. Provides some support for Z as documented in the paper Z and HOL. The source files for various Z specifications in HOL are available via anonymous FTP.
HIPPO Z type-checker using ML in compressed Unix tar format.
HOL-Z tool. A shallow embedding of Z in the higher-order logic theorem prover Isabelle. Also mirrored here and here. See also ZETA.
HTML: mathematical extensions to the World Wide Web HyperText Markup Languge including support for Z by WWW browsers. Please contact Phillip M. Hallam-Baker on hallam@alws.cern.ch if you are interested in this. See also, local information.
JAPE (Just Another Proof Editor) by Bernard Sufrin and Richard Bornat supports typed set theory (Z).
Mathias Mathematics in Animation Suite, including advice on using it to animate Z and references to papers on Suzan (the Surrey Z Animation project).
MATHS Project Z syntax for tool developers, produced as part of a larger effort on samples of syntax description in general. See also MATHS source Z syntax.
Moby/OZ, a graphical editor to build Z and Object-Z specifications.
Nitpick is a freely available tool for fully automatically analyzing software specifications in (roughly) a subset of Z.
OOZE, an object-oriented Z environment.
PiZA, a Prolog Z animator.
Possum - interpreter/animator of Z.
PRECC Z grammar for use with the PRECC compiler-compiler tool is available for use under Unix and MS-DOS.
ProofPower, an industrial strength Z theorem prover based on Higher Order Logic, is available from ICL. Contact ProofPower-support@win.icl.co.uk for further information. See also some brief information on proof infrastructure for Z using HOL.
RoZeLink - The Rose Formaliser Link, from Headway Software. Combines Unified Modeling Language (UML) and the Z notation for formal modelling. See an example and free software download for evaluation.
TrueType Z fonts are available for use under MS Windows (in pkzip format):
- Zed font for Windows and Macintosh by Richard Jones, Computing Laboratory, University of Kent at Canterbury, UK. PostScript Type 1 and TrueType formats.
- Another Z font.
- VDM/Z font from the NPL Data Security Group.
Wizard, a type-checker for Object-Z specifications in L^ATEX.
Z2HTML translator from LaTeX to HTML (also here). See Z notation examples (also here).
ZETA, an open environment based Z, providing an integration framework for tools to edit, browse, analyse, and animate Z specifications. Tools currently integrated into ZETA are the type checker ESZ, the Z compiler ZAP, and adaptors for third-party tools such as the prover Isabelle/HOL-Z and the model-checker SMV.
ZAST (Z Abstract Syntax Tree Viewer). Based on a PreCC Z grammar. Runs under Microsoft Windows 95 and Window NT.
Z Browser is available for use under Windows on PCs. See also Z Browser Plug-in for viewing Z using WWW browsers such as Netscape Navigator and Internet Explorer under Windows 95 and Windows NT.
Zeus WYSIWYG toolset based on Framemaker and Z/EVES. Prototype available by email.
Z/EVES, proving a Z front-end to the EVES proof tool based on ZF set theory from ORA, Canada, is available via on-line distribution.
Zola, a commercial WYSIWYG editor, type-checker and tactical prover for Z from IST, UK.
ZTC is a Z type-checker available free of charge for educational and non-profit uses. It is intended to be ZRM2 compliant. It accepts L^ATEX with zed or oz styles, and ZSL - an ASCII version of Z. ZANS is a Z animator. It is a research prototype that is still very crude. Both ZTC and ZANS run on Linux, SunOS 4.x, Solaris 2.x, Windows 95 and NT 4.0. They are available on-line in the directories ZANS and ZTC. Contact Xiaoping Jia on jia@cs.depaul.edu for further information. ZTC and ZANS information also available here.

Z and VDM

VDM (Vienna Development Method) is a method which uses a specification notation that is similar to Z. See Understanding the differences between VDM and Z and messages relating to comparing VDM and Z which appeared on the comp.software-eng newsgroup.

VDM is discussed on the (unmoderated) VDM forum mailing list. Send an email message containing the command ``join vdm-forum name'' where ``name'' is your real name to mailbase@mailbase.ac.uk. To contact the list administrator, email John Fitzgerald at the University of Newcastle upon Tyne, England, on vdm-forum-request@mailbase.ac.uk. See also other information on VDM.

See Integration of Z and VDM project, SVRC, Queensland, Australia. A new syntax called ViZ (VDM-SL Integrated with Z) has been designed, with a denotational semantics.

Other information

Information on object-oriented extensions of Z, such as Object-Z, Z++ (see also dictionary entry) and ZEST (Z Extended with STructuring), and prototyping Z specifications is available elsewhere. See the book Object Orientation in Z, including further hyperlinks and a bibliography.