.Open The Formal Specification Language Z
. Introduction
The Z (pronounced `Zed`) language is a formal specification language that 
makes it easier to write mathematical description of complex dynamic 
systems such as software.  The descriptions are usually smaller and simpler 
than any programming language can provide. They should contain a mixture of 
formal and informal parts.

Z was developed in Paris, France and Oxford, England.

(Z intro and examples):  
.See http://staff.washington.edu/~jon/z/z-examples.html
. Z Archive
.See http://www.comlab.ox.ac.uk/archive/z.html/
(under rennovation July 2003)

Also see
.See http://vl.zuser.org/

. Z Reference Manual
.Open Spivey01
 J H Spivey 
 The Z Notation: A Reference Manual (online)
 Web 2001 
.See http://spivey.oriel.ox.ac.uk/mike/zrm/index.html
 =handbook formal logic Z SPECIFICATION
 
 Earlier was 
.See [Spivey89]  
.See [Spivey92] 
.Box Quote from web site
The Z Reference Manual has now been allowed to go out of print by the publisher, Prentice Hall, but they have kindly returned the copyright to me, so I can make the full text available here.

Please note that I have not placed the copyright of this work in the public domain. Nevertheless, I freely grant permission to make copies of the whole work for any purpose except direct commercial gain. I retain all other rights, including but not limited to the right to make translations and derivative works, and the right to make extracts and copies of parts of the work. Fair quotation is permitted according to usual scholarly conventions.
.Close.Box
.Close
. Z Glossary
.See http://www/dick/samples/z.glossary.html
. Z Syntax
.See http://www/dick/samples/z.syntax.html

A minor problem with the spread of Z is that it is designed as language
to be written rather than as a language to be input into a computer.
Thus Z users often have to learn a version of the LaTeX mathematical
type-setting language.  On the other hand it makes the expressions much
shorter and clearer than using ASCII.  There are a few resources for
people who want an ASCII form of Z:

Proposed standard lexemes for ASCII/EMail:
.See http://www.csci.csusb.edu/dick/samples/z.lexis.html
and PiZA
.See http://www.noodles.demon.co.uk/PiZA/PiZAHome.html
. Z Semantics
.Set
   JM Spivey
   Understanding Z:A Specification language and its Formal Semantics
   Cambridge Tracts on Theoretical Computer Science 3 Cambridge U press UK 1988
.Close.Set
. Z Rattle Bags of examples etc
.See http://www.csci.csusb.edu/dick/cs320/z/
.See http://www.csci.csusb.edu/dick/methods.html#Z
.See http://www.csci.csusb.edu/dick/cs320/z/zguide.tex

. Standard Z
.See http://www.lemma-one.com/zstan_docs/
.See http://web.comlab.ox.ac.uk/oucl/research/groups/zstandards/

Local:
.See http://www.csci.csusb.edu/dick/cs320/z/zstandard1.0.dvi
.See http://www.csci.csusb.edu/dick/cs320/z/z.part1.ps.Z
.See http://www.csci.csusb.edu/dick/cs320/z/z.part2.ps.Z

Proposed standard lexemes for ASCII/EMail:
.See http://www.csci.csusb.edu/dick/samples/z.lexis.html

. Z FAQ
.See http://www/dick/doc/z.FAQ

. Z Fonts
The online manual
.See http://spivey.oriel.ox.ac.uk/mike/zrm/index.html
has links to useful fonts and styles for LaTex.

UK
.See http://www.cs.ukc.ac.uk/people/staff/rej/Zedfont/latest/
.See http://ftp.comlab.ox.ac.uk/pub/Zforum/zfont.zip
.See http://ftp.ess.npl.co.uk/pub/dsg/vdmzfont/
A true type Z and VDM font is available from the Data Security Group ftp site: 
.See http://www.npl.co.uk/~dsg/index.html
.See ftp://ftp.npl.co.uk/pub/dsg/

Finland:
Here's a file called "lib.tar.gz" which has some fonts in it.
.See http://www.to.icl.fi/ICLE/ProofPower/xemacs/index.htm

USA
Text:
.See http://www.csci.csusb.edu/dick/cs320/z/Zedfont.README
, BinHexed for Mac:
.See http://www.csci.csusb.edu/dick/cs320/z/Zedfont.sea.hqx
, Windows
.See http://www.csci.csusb.edu/dick/cs320/z/Zedfont.zip.uue
.See http://www.csci.csusb.edu/dick/cs320/z/windows.font.uu
. Z Tools
.See http://www.csci.csusb.edu/dick/cs320/z/tools
.See http://www.csci.csusb.edu/dick/cs320/z/ztools.ms

. C++ to Z  
.See http://www.dit.upm.es
. Z People
.See http://www.comlab.ox.ac.uk/oucl/people/

jonathan.bowen
.See http://www.comlab.ox.ac.uk/oucl/people/jonathan.bowen.html
	
Roger Jones, at home: rbj@campion.demon.co.uk
.See http://www.to.icl.fi/ICLE/rbjpub/rbj.htm

. VDM vs Z
.See http://www.comlab.ox.ac.uk/archive/z.html#vdm
.See http://www.cs.man.ac.uk/csonly/cstechrep/Abstracts/UMCS-93-8-1.html

.See [HayesJonesNichols94]


. Z via Tex and HTML
zed.sty
.See http://www.comlab.ox.ac.uk/archive/z/html-z.html

. Tools for Z
.See http://www.comlab.ox.ac.uk/archive/z.html#tools 
.See http://www.csci.csusb.edu/dick/cs320/z/tools
.See http://www.csci.csusb.edu/dick/cs320/z/ztools.ms
. C++ to Z  
.See http://www.dit.upm.es
. Books and Papers
.See http://www.comlab.ox.ac.uk/archive/z/bib.html

Local bibliographic items can be found by selecting:
.See http://www.csci.csusb.edu/dick/bib.php?search=%20Z%20

. Usenet newsgroup
comp.specification.z
.See news://comp.specification.z
. FAQs
Jonathon Bowen's Official comp.specification.z FAQ is in the UK
.See ftp://ftp.comlab.ox.ac.uk/pub/Zforum/faq.

My copy (USA) is 
.See http://www/dick/doc/z.FAQ
. EMail archive
archive-server@comlab.ox.ak.uk
.See mailto:archive-server@comlab.ox.ak.uk

.Close Z