🚀 go-pugleaf

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