dm@.com (Dave Mankins) (03/05/90)
I would appreciate recommendations of texts or articles which are good introductions to the Vienna Development Method or Z. -- david mankins (dm@think.com)
jon@cs.washington.edu (Jon Jacky) (03/06/90)
> 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
goun@loiosh.enet.dec.com (Roger H. Goun) (03/07/90)
Formal Methods: Theory and Practice, P.N. Scharbach, ed., Information
Technology
Research Unit, BP Research Centre, Sunbury-on-Thames, U.K., CRC Press,
1989, ISBN
0-8493-7140-6.
Would anyone who has read this book care to comment on it?
UUCP: ...!decwrl!ddif.enet!goun Roger H. Goun
Internet: goun@ddif.enet.dec.com Digital Equipment Corporation
goun%ddif.enet@decwrl.dec.com 110 Spit Brook Road, ZKO2-2/O23
Nashua, NH 03062 USA
+1 603 881 0022mjl@cs.rit.edu (03/07/90)
> David Mankins (dm@think.com) asks about recommendations of texts and articles > which are good introductions to VDM or Z I can vouch for the D. C. Ince book "An Introduction to Discrete Mathematics and Formal System Specification" (Oxford University Press, 1988). As the title implies, it is designed for use as a text, but can also serve for self study (the existence of exercises is a definite plus). I agree with Jon Jacky that this is not for those with deep mathematical maturity. It's more a gentle introduction to the underlying mathematics and their application within Z, and is especially useful if you're new to the area or your math skills are a bit rusty. Be forewarned: the book does not cover everything in Z (Ince estimates that he covers about 80%). However, hitting Spivey's books without any preparation is a bit like being catapulted off the deck of an aircraft carrier: you get up to speed quickly, but you might not like the jolt :-). Mike Lutz Rochester Institute of Technology Mike Lutz Rochester Institute of Technology, Rochester NY UUCP: {rutgers,cornell}!rochester!rit!mjl INTERNET: mjl@csrit.edu
cliff@ipse2pt5.uucp (Cliff Jones) (03/15/90)
Newsgroups: comp.specification
Subject: Re: recommended texts
Summary:
Expires:
References: <34462@news.Think.COM> <10964@june.cs.washington.edu>
Sender:
Reply-To: cliff@ipse2pt5.UUCP (Cliff Jones)
Followup-To:
Distribution:
Organization: University of Manchester, UK
Keywords:
RE: I read somewhere ...
Jon Jacky is correct, I have just produced a revised version. Info is:
@book{Jones90a,
author = "C. B. Jones",
title = "Systematic Software Development using VDM",
edition = {Second},
publisher = "Prentice Hall International",
year = "1990",
note = "ISBN 13-880733-7"
}
There is a companion "Case Study book":
@book{JonesShaw90,
title = "Case Studies in Systematic Software Development",
editor = "C.B. Jones and R.C.F. Shaw",
publisher = "Prentice Hall International",
year = "1990",
note = "ISBN 13-116088-5
}
A few words of explanation:
New Books on VDM
You may previously have seen "Systematic Software Development using
VDM". This note explains its revised form and a new book of case
studies. Both are available now from Prentice Hall.
The BSI (British Standards Institution) committee on VDM has made
significant progress towards a BSI-VDM standard and this has provided
an incentive to revise my 1986 book. It has also made it worth collecting
some medium-sized case studies and producing two books in a uniform style.
The case studies book ("Case Studies in Systematic Software Development" -
edited by Jones and Shaw) collects together 12 different applications
written by 10 authors. The examples include two database like systems, a
machine architecture, unification, user interface description and garbage
collection as well as two language descriptions (one covering object-oriented
features).
I believe that this book can provide the bridge from the "finger exercises"
which fit in a text book to the larger tasks that students might face in
industrial applications. In the intensive industry courses which I have
prepared, we have always waded into a significant case study. I believe
that this approach should also be used in tertiary education (but recognise
the problems of fitting it into the exams structure).
I hope the availability of the Jones/Shaw book will overcome one of the
limitations of my 1986 book. I have also studied feedback from many people
in planning revisions to the textbook itself.
Apart from the syntactic changes,
I hope that the other visual impact will come from the improved typesetting
and layout. (We now have LaTeX "bsivdm" macros and have produced output on
a high-resolution Linotron printer.) I have used a clearer way of bringing
definitions into proofs and believe this has simplified one of the aspects of
my earlier book which was hardest to teach. The original material on
operation decomposition was unclear and Chapter 10 has been completely
rewritten.
A new Chapter 11 presents a mini-casestudy so as to tie together all parts of
the specification and development method.
The use of BSI-VDM is emphasised by an appendix giving its concrete syntax
(the LaTeX macros actually make it easy to change syntax; it would - for
example - be straightforward to redefine things to produce output in the
limited ASCII syntax). A host of minor corrections and improvements have also
been incorporated in the second edition.
I am currently revising the "Teacher's Notes" and these will be available in
Spring 1990. This time, they will be distributed from PHI.
Cliff Jones