[Lemma 1]

Z Standards Documents

Lemma 1 is closely involved with the initiative to standardise the Z notation. The Z Standards Panel has its own web pages and an FTP site where you can obtain a copy of the draft standard. There is also a central list of documents relevant to the Z Standards maintained by Andrew Martin .

This page is a personal collection of documents and links relating to the standards work maintained at the Lemma 1 Ltd. web site by me, Rob Arthan. Jonathan Bowen provides an excellent site for formal methods generally and Z in particular.

The following two papers describe the current (agreed!) position on two important issues for Z.; you can also find these and many others at the Z standards FTP site

The following brief note discusses the syntactic status of some of the Z tool kit operators. The recommendations of this note would let you write things like "max (dom f)" or "#(dom f)" without those irritating brackets.

The following paper, generally referred to as "the ancient paper on concrete syntax", may still be of interest. It covers rather more than the title suggests and some of the issues it raises are still contentious.

The theory of the free types mechanism is discussed in the following papers:

Ian Toyn is the acting project editor for the Z Standard. Ian has been recording his perspective on the current state-of-the-art in a series of draft documents that you can find in his collection of documents relating to the standards work. The semantic equations in Ian's work are given using a Z-like surface syntax for untyped first-order set theory. The following paper of mine contains an adaptation of this semantics into type-checked Z:

While not concerned with the Z standardisation directly, the following paper, written for a workshop on undefinedness and partiality at CADE-13 may also be of interest:

The slides of a presentation of the undefinedness paper are also available (in HTML/JPEG format).

All of the papers are in PostScript format.

Created by  Rob Arthan [rda at lemma-one dot com]
Last updated: $Date: 2003/04/22 17:01:40 $
[Lemma 1]