Path: utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!swrinde!zaphod.mps.ohio-state.edu!think!snorkelwacker!mit-eddie!uw-beaver!uw-june!jon From: jon@cs.washington.edu (Jon Jacky) Newsgroups: comp.specification Subject: Re: recommended texts Summary: Z and VDM textbooks, articles recommended Message-ID: <10964@june.cs.washington.edu> Date: 5 Mar 90 18:59:59 GMT References: <34462@news.Think.COM> Organization: U of Washington, Computer Science, Seattle Lines: 112 > 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