There is now a large collection of books (and articles) available which provide an introduction to Z and its use. Specification Case Studies edited by Hayes [107] served as an early definition of the language and contained many examples of particular aspects of the notation. This was followed by Spivey's The Z Notation: A Reference Manual [187,188] which came to be the de facto definition of the language, and in [186] Spivey provides a semantics.
Z soon became commonplace in the CS undergraduate curriculum, and this led to the publication of many books providing an introduction to Z. These include An Introduction to Formal Specification and Z by Potter et al [166] and books by Ratcliff [169], Bottaci and Jones [29], Bowen [30] and Jacky [126].
Two more advanced books are also worth mentioning. Z in Practice [15] by Barden, Stepney and Cooper was aimed at those who already understood the basics of Z, and Using Z: Specification, Refinement and Proof [209] by Woodcock and Davies looks at proof and refinement in Z in some detail.
Using Z acts as a precursor to this book in many ways, and there is an overlap in some of the material covered in Chapters 1 to 4 of this book with that in [209]. Many of the later refinement examples in [209] are particularly interesting and motivated some of the generalisations to refinement discussed below.
There is also a regular series of conferences, ZUM: The Z Formal Specification Notation, devoted to Z, see, for example, [164,36,33,34,35,32,31], and the FME conferences (e.g., [95,90]) also regularly contain papers concerning aspects of the notation.
More details of publications, tools etc. can be found on the extensive information resource which is collated on the WWW at:
http://archive.comlab.ox.ac.uk/z.html