🚀 go-pugleaf

> David Mankins (dm@think.com) asks about recommendations of texts and articles
> which are good introductions to VDM or Z

Here are personal opinions about some of the references I've used:

The best introduction to Z is:

Specification Case Studies, Ian Hayes (editor), Prentice-Hall 1987, ISBN
0-13-826579-8

This is a series of relatively short examples of graduated difficulty.  Some
are reprints of journal papers.  One of the most instructive of these is:

Specification of the UNIX file system, by Carroll Morgan and Bernard Sufrin,
IEEE Transactions on Software Engineering, vol SE-10, no 2, March 1984, pps.
128 - 142.

Another recent journal paper of instructive value, which is not included
in the Hayes volume, is:

The Formal Specification of a Small Bookshop Information System, by David Gray,
IEEE Transactions on Software Engineering, 14(2), Feb 1988, 263 - 272.

There was also a special section on Z in the British journal, Software
Engineering Journal, 4(1) January 1989.  The articles aren't as good as those
in the Hayes book and the others I've mentioned, except one: An Introduction to
Z and Formal Specifications, by J.M. Spivey, which is a good tutorial. 
Actually it's probably the best first thing to read about Z.   That paper also
appears in slightly different form in:

The Z Notation, A Reference Manual by J.M. Spivey; Prentice-Hall 1989, ISBN
0-13-983768-X

The above volume has some tutorial material (like the reprint of the journal
article) but overall it really is a reference manual, not a tutor, and is
pretty dense, without much guidance about how or why to apply the stuff.
However, if you plan to experiment with Z you've got to have it.

Then there is:

Understanding Z: A Specification Language and its Formal Semantics, by J.M.
Spivey, Cambridge University Press, 1988.

An odd book that contains a mix of stuff --- a version of the tutorial example
that also appears in Spivey's other works, and a comparison of Z to other
formal notations, including VDM.  The heart of the book is a long formal
specification of Z itself (in Z --- what else?).  This last, frankly, is pretty
daunting, much much harder to understand than, say, the Unix specification.

One of the appeals of Z is that it is being picked up outside the group that
originated it (unlike most of the other formal specification languages).  I
recently saw a new textbook in a bookstore,  Software Engineering Mathematics,
by Woodcock and Loomes. I think the publisher was Addison-Wesley, 1989.  Its
cover bore the Software Engineering Institute logo and it said something like
"SEI Series on Software Engineering", for what that's worth.  It looked pretty
good.   It was basically a textbook in predicate calculus and set theory, with
a short survey of several formal methods, but it emphasized Z, in fact the
whole book used what looked a lot like Z as "the" notation of the book.   There
is also a new book called An Introduction to Discrete Mathematics and Formal
System Specification by D.C. Ince,  Clarendon Press. The first part was about
predicate calculus and set theory, and the second half  was a Z textbook.  I
got a better impression of Woodcock and Loomes, possibly because that one
seemed pitched at a more mature audience, but be warned I didn't have time to
read either one thoroughly.

A good introduction to formal specifcation in general is:

The Specification of Complex Systems by B. Cohen, W.T. Harwood, and M.I.
Jackson, Addison Wesley 1986.  

It discusses several notations, not including Z, but including VDM ("the Vienna
Development Method") which is rather similar (see Spivey's Understanding Z for
an explicit comparison).  In fact this book was much clearer and convincing to
me about VDM than the several books by Cliff Jones, its main exponent.   VDM is
about the only notation besides Z which seems to be getting much application
outside its originating research group. (The most recent of Jones' books on Z
is Systematic Software Development Using VDM, Cliff B. Jones, Prentice Hall,
1986.  I read somewhere that a new edition of this book was planned, to include
or conform to the new British Standards Institute (BSI) "standard" VDM
definition.

If you take a look at the books and decide you want to see more, there is an
electronic newsletter about Z that is very infrequently distributed over the
Internet.  To get added to the list, write to
zforum%prg.oxford.ac.uk@nsfnet-relay.ac.uk.   Back issues of Z Forum, and lots
of other stuff about Z, including bibliographies and manuscripts, are available
from the archives at Oxford.   If you want to get started with this, send a
message to  archive-server%uk.ac.oxford.prg@relay.mod.uk that simply includes
on a single line, the command "help".

Writing Z specifications presents challenges, since it is emphatically
non-ASCII.  It uses a lot of arcane symbology from mathematics and in addition
likes to draw boxes around things.  Mike Spivey created a set of LaTeX macros
in a file called "zed.sty" which I got from the Oxford archives.   Later,
Spivey created a newer Z tool called "fuzz" (by analogy with Unix "lint") which
includes newer, better LateX macros, plus a type checker and cross-referencer.
     
"Fuzz" uses the LaTeX source for Z also as the input source code for these
latter tools.  So this LaTeX source provides a way to write Z in ASCII. 
Fuzz is a product which Mike sells for a few hundred dollars, versions are
available for IBM PC's and Sun's, other platforms by special request (it says
here).  (I haven't tried or seen "Fuzz.")

(I started looking into formal specification languages to help with
specifying software for the control system of a medical cyclotron used for
neutron radiation therapy for cancer and isotope production.  I've decided to
use Z to specify a lot of it, although Z can't describe it all.)

- Jon Jacky             	(206)-548-4117
Radiation Oncology RC-08	jon@gaffer.rad.washington.edu
University of Washington
Seattle, WA  98195