[Z User Group - ZUG] [Centre for Applied Formal Methods (CAFM), South Bank University, London, UK] * Formal Methods * Object-Z * B-Method

The Z notation

! Next conference: ABZ 2008, London, UK, 16-18 September 2008.
Last ZB conference: ZB2005, UK, 13-15 April 2005

Community Z Tools Project (CZT) at SourceForge

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:

Interactive forms (if supported by your WWW client):

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 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 (also less up-to-date here) 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-integraity 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 and this version will be maintained in future, although it is mainly of historical interest. However, some files may still be useful. 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 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 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. and 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 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.software-eng and the moderated comp.risks Z User Meetings are announced in the newsgroup news.announce.conferences as well.

Publications

An online 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.

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 PDF format) is available online.

The following online WWW pages associated with Z books are available:

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.

Finally, for those interested in the history of Z, see some early history information from Carroll Morgan.

Z standardization

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. See also Z standards drafts and proposals. A printed copy of Version 1.0 of the Z Base Standard (an early version) is available as PRG Technical Monograph PRG-107. New FTP information concerning the standard is installed as it becomes available. Further developments are still under consideration. For further information, see: 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.

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.

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 first combined "ZB" conference, ZB2000, was held in conjunction with the B-Method community at York, UK, 29 August - 2 September 2000.

ZB2002 was held at Grenoble, France, 23-25 January 2002.

ZB2003 was held at Turku, Finland, 4-6 June 2003.

The last main conference was ZB2005, Guildford, UK, 13-15 April 2005. 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 online.

See also information on other formal methods meetings.

Courses

There are various courses at OUCL which include the teaching of Z. Logica offer a 5 day course on Formal Software Specification using Z.

Tool support

See Community Z Tools Project (CZT) proposal, started September 2001. This is now an open source project under SourceForge.

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

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

The following Z tools are also available: See also:

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.

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

See also a comparison of Z, VDM and the B-Method.

Other information

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.

See also:

For some entirely different and unrelated "Z" links, if you are tired of the "real" thing, see:

[Top]
Comments, corrections and new information are gratefully received.

Part of the LSBU Museophile archive.
See also information on other formal methods and notations.
Last updated by Jonathan Bowen, 16 January 2006.