🚀 go-pugleaf

In article <592@bohra.cpg.oz> mike@bohra.cpg.oz (Mike Crooks) writes:
>Could someone please point me at some references to the 'Z' specification
>language developed at Oxford.

There are now several good books on the subject - I particularly like
the one on Z semantics - the name of which escapes me for the moment.
However, the book you should really read is the Z Manual by Mike Spivey
published by Prentice Hall in the Hoare series (my that is a fine series
Helen).

Steven.



-- 
Steven Ericsson Zenith              *            email: zenith@cs.yale.edu
Fax: (203) 466 2768                 |            voice: (203) 432 1278
"The tower should warn the people not to believe in it." - P.D.Ouspensky
Yale University Dept of Computer Science 51 Prospect St New Haven CT 06520 USA

mike@bohra.cpg.oz (Mike Crooks) writes:

>Could someone please point me at some references to the 'Z' specification
>language developed at Oxford.

Specification Case Studies 
Ian Hayes (editor)
Prentice Hall
--
Anthony Lee (Michaelangelo teenage mutant ninja turtle) (Time Lord Doctor) 
ACSnet:	anthony@batserver.cs.uq.oz	TEL:+(61)-7-371-2651
Internet: anthony@batserver.cs.uq.oz.au	    +(61)-7-377-4139 (w)
SNAIL: Dept Comp. Science, University of Qld, St Lucia, Qld 4072, Australia

From article <592@bohra.cpg.oz>, by mike@bohra.cpg.oz (Mike Crooks):
> Could someone please point me at some references to the 'Z' specification
> language developed at Oxford.

From the PRG Z bibliography:

@techreport{bowen:fullzbib,
        author = "Jonathan P. Bowen and Ruaridh Macdonald",
        title = "Z Bibliography",
        institution = "Programming Research Group, Oxford University",
        address = "Oxford, UK",
        year = "1988",
        month = "December",
        note = "A master bibliography of both published and unpublished work
related to Z. This is available via electronic mail by sending a
message of ``send z zbib'' to <archive-server@uk.ac.oxford.prg>
on JANET. (For more information on the archive server, send a
message of ``help''.)"}

@book{hayes:specification,
        author = "Ian J. Hayes",
        title = "Specification Case Studies",
        series = "International Series in Computer Science",
        publisher = "Prentice-Hall",
        year = "1987",
        note = "ISBN 0-13-826579-8, ISBN 0-13-826595-X PBK"}

@techreport{sking:zgrammar,
        author = "Steve King and Ib H. S\o{}rensen and James C.P. Woodcock",
        title = "Z: Grammar and Concrete and Abstract Syntaxes",
        institution = "Programming Research Group, Oxford University",
        address = "Oxford, UK",
        year = "1988",
        type = "Technical Monograph",
        number = "PRG-68",
        note = "ISBN 0902928503"}

@book{spivey:znotation,
        author = "J. Michael Spivey",
        title = "The Z Notation: A Reference Manual",
        publisher = "Prentice-Hall",
        series = "International Series in Computer Science",
        year = "1989",
        note = "ISBN 013983768X"}

@book{spivey:understandingz,
        author = "J. Michael Spivey",
        title = "Understanding Z: A Specification Language and its Formal Semantics",
        publisher = "Cambridge University Press",
        year = "1988",
        month = "January",
        note = "Published version of 1985 D.Phil. thesis."}

I am not a mathematician and I find "Understanding Z" is quite difficult.

A good introduction to set theory and predicate calculus is:
@book{woodcock:maths,
        author = "James C.P. Woodcock and Martin Loomes",
        title = "Software Engineering Mathematics: Formal Methods Demystified",
        publisher = "Pitman Publishing Ltd",
        address = "London, UK",
        year = "1988",
        note = "ISBN 0273026739"}

This book uses the concrete syntax of Z and is a good introduction.

Used fivers will do nicely thanks Jim :-)

  ____________________________________________________________________
  Pete Young         pyoung@axion.bt.co.uk        Phone +44 473 645054
  British Telecom Research Labs,SSTF, Martlesham Heath IPSWICH IP5 7RE

Several postings on this subject have noted the three essential references:
Hayes' (ed.) SPECIFICATION CASE STUDIES, Woodcock and Loomes' SOFTWARE
ENGINEERING MATHEMATICS, and Spivey's THE Z NOTATION: A REFERENCE MANUAL. 

Here is a fourth reference that I have found a useful supplement to the
canonical three:

@article{woodcock:structuringspecs,
	author="J. C. P. Woodcock",
	title="Structuring Specifications in Z",
	journal="Software Engineering Journal",
	volume=4,
	number=1,
	month="January",
	year=1989,
	pages="51--66"}	
	
This article is an extended tutorial on the schema calculus. It gives a 
lengthier treatment, with examples, of several features that are  touched on
only briefly in Spivey's book, and are used but not explained very thoroughly
in some of the Hayes studies.  These topics include use of "bindings" (theta
expressions), schema quantification, schemas used as types, as predicates, and
as hypotheses in theorems, component renaming, hiding,  schema composition, and
precondition investigation.  The article is similar in style to SOFTWARE
ENGINEERING MATHEMATICS and elaborates an example introduced in that book.  

The article appears in a special journal issue devoted to the Z notation.

Jon Jacky, University of Washington, Seattle  jon@gaffer.rad.washington.edu

Two other recent references which may be useful for those interested
in the latest developments and research concerned with Z:

@proceedings{VDM90,
  editor = {D. Bj{\o}rner and C.A.R. Hoare and H. Langmaack},
  title = {{VDM} and {Z} -- Formal Methods in Software Development},
  publisher = {Springer-Verlag},
  address = {Berlin, Germany},
  series = {Lecture Notes in Computer Science},
  volume = {428},
  year = {1990},
  isbn = {3-540-52513-0 and 0-387-52513-0},
  note = {Proceedings of Third Interational Symposium of VDM Europe,
    17--21 April 1990, Kiel, Germany.}
}

@proceedings{Z90,
  editor = {J.E. Nicholls},
  title = {{Z} User Workshop},
  publisher = {Springer-Verlag},
  address = {Berlin, Germany},
  organization = {Programming Research Group, Oxford University, UK},
  series = {Workshops in Computing},
  length = {288},
  month = {September},
  year = {1990},
  isbn = {3-540-19627},
  note = {Proceedings of the Fourth Annual Z User Meeting,
    15 December 1989, Oxford, UK.
    Price \pounds24.00 soft cover (BCS members \pounds19.00).}
}

--
Jonathan Bowen, PRG, Oxford University

The best book on Z by far is:

Antoni Diller
Z: An Introduction to Formal Methods
Chichester, Wiley, 1990
ISBN 0 471 92489 X