@STRING{oucl	= "Oxford University Computing Laboratory" }
@STRING{oxford	= "Wolfson Building, Parks Road, Oxford, UK" }
@STRING{uk	= "UK" }
@STRING{lncs	= "Lecture Notes in Computer Science" }

@Misc{		  z:00bib2,
  key		= {00bibliography2},
  title		= {{Z} Extra Bibliography},
  howpublished	= {URL: \verb"http://www.comlab.ox.ac.uk/archive/z/bib.html"},
  year		= {1990 onwards},
  url		= {http://www.comlab.ox.ac.uk/archive/z/bib.html},
  annote	= {This bibliography is maintained in \BibTeX\ database
		  source format accessible in searchable form on the World
		  Wide Web. To add entries, please send as complete
		  information as possible to Jonathan Bowen on
		  \verb"J.P.Bowen@reading.ac.uk".},
  comment	= {Extra Z Bibliography in BibTeX database format.
		  
		  See also "Master Z Bibliography". The entries included here
		  are not included in the "Select Z Bibliography" printed in
		  the Z User Meeting proceedings, but may be of interest.
		  
		  Maintained by Jonathan Bowen.
		  
		  The University of Reading, Department of Computer Science,
		  Whiteknights, PO Box 225, Reading, Berks RG6 6AY, England.
		  Tel: +44-1734-316544. Fax: +44-1734-751994. Email:
		  J.P.Bowen@reading.ac.uk
		  
		  Please send new entries to Jonathan Bowen.
		  
		  Copyright (C) 1994-1998 Jonathan Bowen. All rights reserved.
		  
		  Last updated 4 August 1998.
		  
		  Entries not included in the Master Z Bibliography
		  \cite{z:00bib} may be in this alternative Z Bibliography
		  file. This includes older unpublished documents such as
		  technical reports, MSc theses, draft papers, etc.,
		  particularly if they have subsequently been published
		  elsewhere.}
}

@TechReport{	  z:abow89b,
  author	= {G. D. Abowd and J. P. Bowen and A. J. Dix and M. D.
		  Harrison and R. Took},
  title		= {User Interface Languages: A survey of existing methods},
  institution	= oucl,
  address	= oxford,
  type		= {Technical Report},
  number	= {PRG-TR-5-89},
  url		= {http://www.comlab.ox.ac.uk/oucl/publications/tr/TR-5-89.html}
		  ,
  length	= 65,
  month		= oct,
  year		= 1989,
  other		= {Alan Dix, Michael Harrison and Roger Took are members of
		  the Human Computer Interaction Group, Department of
		  Computer Science, University of York. This report was
		  originally produced as part of ESPRIT II project no.\ 2487:
		  `REDO: Maintenance, Validation and Documentation of
		  Software Systems.' It covers a number of methods, including
		  a chapter on modelling using Z.}
}

@TechReport{	  z:abow89b,
  author	= {G. D. Abowd and J. P. Bowen and A. J. Dix and M. D.
		  Harrison and R. Took},
  title		= {User Interface Languages: A survey of existing methods},
  institution	= oucl,
  address	= oxford,
  type		= {Technical Report},
  number	= {PRG-TR-5-89},
  url		= {http://www.comlab.ox.ac.uk/oucl/publications/tr/TR-5-89.html}
		  ,
  length	= 65,
  month		= oct,
  year		= 1989,
  other		= {Alan Dix, Michael Harrison and Roger Took are members of
		  the Human Computer Interaction Group, Department of
		  Computer Science, University of York. This report was
		  originally produced as part of ESPRIT II project no.\ 2487:
		  `REDO: Maintenance, Validation and Documentation of
		  Software Systems.' It covers a number of methods, including
		  a chapter on modelling using Z.}
}

@TechReport{	  z:amma93,
  author	= {P. Ammann and J. Offutt},
  title		= {Functional and Test Specifications for the {Mistix} File
		  System},
  type		= {Technical Report},
  number	= {ISSE-TR-93-100},
  institution	= {Department of Information \& Software Systems Engineering,
		  George Mason University},
  address	= {USA},
  url		= {file://isse.gmu.edu/pub/techrep/ammann_93_100_ps.Z},
  month		= jan,
  year		= 1993,
  abstract	= {Mistix is a simple file system based on the Unix file
		  system. Mistix is used in classroom exercises in graduate
		  software engineering classes at George Mason University. In
		  this document, we supply several different specifications
		  for Mistix. First we give an informal specification. Next,
		  since the informal specification turns out to be difficult
		  to formalize directly, we supply a revised informal
		  specification that matches subsequent formal
		  specifications. We give a model-based specification for
		  Mistix in Z, followed by functional test specifications
		  based on the Category-Partition method. Finally, we give an
		  algebraic specification for Mistix.}
}

@TechReport{	  z:amma93,
  author	= {P. Ammann and J. Offutt},
  title		= {Functional and Test Specifications for the {Mistix} File
		  System},
  type		= {Technical Report},
  number	= {ISSE-TR-93-100},
  institution	= {Department of Information \& Software Systems Engineering,
		  George Mason University},
  address	= {USA},
  url		= {file://isse.gmu.edu/pub/techrep/ammann_93_100_ps.Z},
  month		= jan,
  year		= 1993,
  abstract	= {Mistix is a simple file system based on the Unix file
		  system. Mistix is used in classroom exercises in graduate
		  software engineering classes at George Mason University. In
		  this document, we supply several different specifications
		  for Mistix. First we give an informal specification. Next,
		  since the informal specification turns out to be difficult
		  to formalize directly, we supply a revised informal
		  specification that matches subsequent formal
		  specifications. We give a model-based specification for
		  Mistix in Z, followed by functional test specifications
		  based on the Category-Partition method. Finally, we give an
		  algebraic specification for Mistix.}
}

@TechReport{	  z:amma93b,
  author	= {P. Ammann and J. Offutt},
  title		= {Using Formal Methods To Mechanize Category-Partition
		  Testing},
  type		= {Technical Report},
  number	= {ISSE-TR-93-105},
  institution	= {Department of Information \& Software Systems Engineering,
		  George Mason University},
  address	= {USA},
  url		= {file://isse.gmu.edu/pub/techrep/ammann_93_105_ps.Z},
  month		= sep,
  year		= 1993,
  abstract	= {We extend the category-partition method, a
		  specification-based method for testing software. Previous
		  work in category-partition has focused on developing
		  structured test specifications that describe software
		  tests. We offer guidance in making the important decisions
		  involved in transforming test specifications to actual test
		  cases. We present a structured approach to making those
		  decisions, including a mechanical procedure for test
		  derivation. With this procedure, we suggest a heuristic for
		  choosing a minimal coverage of the categories identified in
		  the test specifications, suggest parts of the process that
		  can be automated, and offer a solution to the problem of
		  identifying infeasible combinations of test case values.
		  Our method uses formal schema-based functional
		  specifications and is illustrated with an example of a
		  simple file system. We conclude that our approach eases
		  test case creation and leads to effective tests of
		  software. We also note that by basing this procedure on
		  formal specifications, we can identify anomalies in the
		  functional specifications.}
}

@TechReport{	  z:amma93b,
  author	= {P. Ammann and J. Offutt},
  title		= {Using Formal Methods To Mechanize Category-Partition
		  Testing},
  type		= {Technical Report},
  number	= {ISSE-TR-93-105},
  institution	= {Department of Information \& Software Systems Engineering,
		  George Mason University},
  address	= {USA},
  url		= {file://isse.gmu.edu/pub/techrep/ammann_93_105_ps.Z},
  month		= sep,
  year		= 1993,
  abstract	= {We extend the category-partition method, a
		  specification-based method for testing software. Previous
		  work in category-partition has focused on developing
		  structured test specifications that describe software
		  tests. We offer guidance in making the important decisions
		  involved in transforming test specifications to actual test
		  cases. We present a structured approach to making those
		  decisions, including a mechanical procedure for test
		  derivation. With this procedure, we suggest a heuristic for
		  choosing a minimal coverage of the categories identified in
		  the test specifications, suggest parts of the process that
		  can be automated, and offer a solution to the problem of
		  identifying infeasible combinations of test case values.
		  Our method uses formal schema-based functional
		  specifications and is illustrated with an example of a
		  simple file system. We conclude that our approach eases
		  test case creation and leads to effective tests of
		  software. We also note that by basing this procedure on
		  formal specifications, we can identify anomalies in the
		  functional specifications.}
}

@TechReport{	  z:arth91b,
  author	= {R. D. Arthan},
  title		= {On Free Type Definitions in {Z}},
  institution	= {ICL Defence Systems},
  address	= uk,
  type		= {Technical Report},
  number	= {DS/\-FMU/\-IED/\-WRK016},
  month		= {April},
  year		= {1991}
}

@Book{		  z:bard94,
  author	= {R. Barden and S. Stepney and D. Cooper},
  title		= {{Z} in Practice (A methods handbook for {Z})},
  publisher	= {Prentice-Hall},
  year		= 1994
}

@TechReport{	  z:baxt88,
  author	= {S. Baxter},
  title		= {Executing {Z} Specifications},
  institution	= {British Telecom Research Laboratories},
  address	= {Martlesham Heath, Ipswich, Suffolk, UK},
  type		= {Research and Technology memorandum},
  number	= {RT31/\-009/\-88},
  year		= {1988}
}

@TechReport{	  z:benv90,
  author	= {M. Benveniste},
  title		= {Operational Semantics of a Distributed Object-Oriented
		  Language and its {Z} Formal Specification},
  institution	= {IRISA/INRIA-Rennes},
  address	= {Campus de Beaulieu, 35042 Rennes C\'edex, France},
  type		= {Rapport de recherche INRIA},
  number	= 1230,
  month		= may,
  year		= 1990
}

@TechReport{	  z:benv90,
  author	= {M. Benveniste},
  title		= {Operational Semantics of a Distributed Object-Oriented
		  Language and its {Z} Formal Specification},
  institution	= {IRISA/INRIA-Rennes},
  address	= {Campus de Beaulieu, 35042 Rennes C\'edex, France},
  type		= {Rapport de recherche INRIA},
  number	= 1230,
  month		= may,
  year		= 1990
}

@TechReport{	  z:best86,
  author	= {M. A. Best},
  title		= {Specification of a {Z} Cross-reference Facility},
  institution	= {IBM United Kingdom Laboratories Ltd.},
  address	= {Hursley Park, Winchester, Hampshire SO21 2JN, UK},
  type		= {{IBM} Technical Report},
  number	= {TR12.253},
  month		= {September},
  year		= {1986}
}

@TechReport{	  z:blyt90,
  author	= {D. Blyth},
  title		= {The {CICS} Application Programming Interface: Temporary
		  storage},
  institution	= {IBM United Kingdom Laboratories Ltd},
  address	= {Hursley Park, Winchester, Hampshire SO21 2JN, UK},
  type		= {{IBM} Technical Report},
  number	= {TR12.301},
  month		= dec,
  year		= 1990,
  annote	= {One of a number of reports on the CICS application
		  programming interface. See also
		  \cite{z:hous90b,z:king90c,z:mund90}.}
}

@TechReport{	  z:blyt90,
  author	= {D. Blyth},
  title		= {The {CICS} Application Programming Interface: Temporary
		  storage},
  institution	= {IBM United Kingdom Laboratories Ltd},
  address	= {Hursley Park, Winchester, Hampshire SO21 2JN, UK},
  type		= {{IBM} Technical Report},
  number	= {TR12.301},
  month		= dec,
  year		= 1990,
  annote	= {One of a number of reports on the CICS application
		  programming interface. See also
		  \cite{z:hous90b,z:king90c,z:mund90}.}
}

@TechReport{	  z:bowe91g,
  author	= {J.P. Bowen and P.T. Breuer and K.C. Lano},
  title		= {The {REDO} Project: Final Report},
  institution	= oucl,
  address	= oxford,
  type		= {Technical Report},
  number	= {PRG-TR-23-91},
  length	= {45},
  month		= {December},
  year		= {1991}
}

@InProceedings{	  z:bowe92b,
  author	= {J. P. Bowen},
  title		= {Select {Z} Bibliography},
  booktitle	= {{Z} User Workshop, {York} 1991},
  editor	= {J. E. Nicholls},
  publisher	= {Springer-Verlag},
  series	= {Workshops in Computing},
  pages		= {367-397},
  year		= {1992}
}

@InProceedings{	  z:bowe92c,
  author	= {J. P. Bowen},
  title		= {{Comp.specification.z} and {Z FORUM} Frequently Asked
		  Questions},
  booktitle	= {{Z} User Workshop, {York} 1991},
  editor	= {J. E. Nicholls},
  publisher	= {Springer-Verlag},
  series	= {Workshops in Computing},
  pages		= {398-401},
  year		= {1992},
  annote	= {This is a published version of the message that is
		  maintained and sent out monthly on the
		  \verb"comp.specification.z" {\sc usenet} newsgroup and
		  ZFORUM electronic mailing list \cite{z:zfor}.}
}

@InProceedings{	  z:bowe93,
  author	= {J. P. Bowen},
  title		= {Select {Z} Bibliography},
  annote	= {},
  crossref	= {z:z93},
  pages		= {309-341}
}

@InProceedings{	  z:bowe93,
  author	= {J. P. Bowen},
  title		= {Select {Z} Bibliography},
  annote	= {},
  crossref	= {z:z93},
  pages		= {309-341}
}

@InProceedings{	  z:bowe93b,
  author	= {J. P. Bowen},
  title		= {{Comp.specification.z} and {Z FORUM} Frequently Asked
		  Questions},
  annote	= {},
  crossref	= {z:z93},
  pages		= {342-347}
}

@InProceedings{	  z:bowe93b,
  author	= {J. P. Bowen},
  title		= {{Comp.specification.z} and {Z FORUM} Frequently Asked
		  Questions},
  annote	= {},
  crossref	= {z:z93},
  pages		= {342-347}
}

@TechReport{	  z:bowe94,
  author	= {J. P. Bowen and M. G. Hinchey},
  title		= {Seven More Myths of Formal Methods},
  institution	= oucl,
  address	= oxford,
  type		= {Technical Report},
  number	= {PRG-TR-7-94},
  length	= 19,
  url		= {http://www.comlab.ox.ac.uk/oucl/publications/tr/TR-7-94.html}
		  ,
  month		= jun,
  year		= 1994,
  annote	= {This article deals with further myths in addition to those
		  presented in \cite{z:hall90b}. See revised versions in
		  \cite{z:bowe95} and {\em IEEE Software}.}
}

@TechReport{	  z:bowe94,
  author	= {J. P. Bowen and M. G. Hinchey},
  title		= {Seven More Myths of Formal Methods},
  institution	= oucl,
  address	= oxford,
  type		= {Technical Report},
  number	= {PRG-TR-7-94},
  length	= 19,
  url		= {http://www.comlab.ox.ac.uk/oucl/publications/tr/TR-7-94.html}
		  ,
  month		= jun,
  year		= 1994,
  annote	= {This article deals with further myths in addition to those
		  presented in \cite{z:hall90b}. See revised versions in
		  \cite{z:bowe95} and {\em IEEE Software}.}
}

@InProceedings{	  z:bowe94c,
  author	= {J. P. Bowen},
  title		= {Select {Z} Bibliography},
  pages		= {359-396},
  annote	= {},
  crossref	= {z:z94},
  url		= {file://ftp.comlab.ox.ac.uk/pub/Zforum/z94.ps.Z}
}

@InProceedings{	  z:bowe94c,
  author	= {J. P. Bowen},
  title		= {Select {Z} Bibliography},
  pages		= {359-396},
  annote	= {},
  crossref	= {z:z94},
  url		= {file://ftp.comlab.ox.ac.uk/pub/Zforum/z94.ps.Z}
}

@InProceedings{	  z:bowe94d,
  author	= {J. P. Bowen},
  title		= {{Comp.specification.z} and {Z FORUM} Frequently Asked
		  Questions},
  pages		= {397-404},
  annote	= {},
  crossref	= {z:z94},
  url		= {file://ftp.comlab.ox.ac.uk/pub/Zforum/faq94.ps.Z}
}

@InProceedings{	  z:bowe94d,
  author	= {J. P. Bowen},
  title		= {{Comp.specification.z} and {Z FORUM} Frequently Asked
		  Questions},
  pages		= {397-404},
  annote	= {},
  crossref	= {z:z94},
  url		= {file://ftp.comlab.ox.ac.uk/pub/Zforum/faq94.ps.Z}
}

@TechReport{	  z:bowe94f,
  author	= {J. P. Bowen and M. G. Hinchey},
  title		= {Ten Commandments of Formal Methods},
  type		= {Technical Report},
  institution	= {University of Cambridge, Computer Laboratory},
  number	= 350,
  address	= uk,
  length	= 18,
  month		= sep,
  year		= 1994,
  url		= {http://www.cl.cam.ac.uk/users/mgh1001/10comms.html},
  note		= {Revised version in {\em IEEE Computer} \cite{z:bowe95b}}
}

@TechReport{	  z:bowe94f,
  author	= {J. P. Bowen and M. G. Hinchey},
  title		= {Ten Commandments of Formal Methods},
  type		= {Technical Report},
  institution	= {University of Cambridge, Computer Laboratory},
  number	= 350,
  address	= uk,
  length	= 18,
  month		= sep,
  year		= 1994,
  url		= {http://www.cl.cam.ac.uk/users/mgh1001/10comms.html},
  note		= {Revised version in {\em IEEE Computer} \cite{z:bowe95b}}
}

@TechReport{	  z:bowe95,
  author	= {J. P. Bowen and M. G. Hinchey},
  title		= {Seven More Myths of Formal Methods},
  type		= {Technical Report},
  number	= 357,
  institution	= {University of Cambridge, Computer Laboratory},
  address	= uk,
  length	= 12,
  url		= {http://www.cl.cam.ac.uk/users/mgh1001/TECHREPORTS/7myths.ps.Z}
		  ,
  month		= jan,
  year		= 1995,
  note		= {Revised version in {\em IEEE Software} \cite{z:bowe95c}},
  annote	= {This article deals with further myths in addition to those
		  presented in \cite{z:hall90b}.}
}

@TechReport{	  z:bowe95,
  author	= {J. P. Bowen and M. G. Hinchey},
  title		= {Seven More Myths of Formal Methods},
  type		= {Technical Report},
  number	= 357,
  institution	= {University of Cambridge, Computer Laboratory},
  address	= uk,
  length	= 12,
  url		= {http://www.cl.cam.ac.uk/users/mgh1001/TECHREPORTS/7myths.ps.Z}
		  ,
  month		= jan,
  year		= 1995,
  note		= {Revised version in {\em IEEE Software} \cite{z:bowe95c}},
  annote	= {This article deals with further myths in addition to those
		  presented in \cite{z:hall90b}.}
}

@InProceedings{	  z:bowe95l,
  author	= {J. P. Bowen},
  title		= {Select {Z} Bibliography},
  pages		= {527-560},
  annote	= {},
  crossref	= {z:z95},
  url		= {ftp://ftp.comlab.ox.ac.uk/pub/Zforum/z95.ps.Z}
}

@InProceedings{	  z:bowe95m,
  author	= {J. P. Bowen},
  title		= {{Comp.specification.z} and {Z FORUM} Frequently Asked
		  Questions},
  pages		= {561-569},
  annote	= {},
  crossref	= {z:z95},
  url		= {ftp://ftp.comlab.ox.ac.uk/pub/Zforum/faq95.ps.Z}
}

@TechReport{	  z:burn89,
  author	= {A. Burns and A. J. Wellings},
  title		= {Priority Inheritance and Message Passing Communication: A
		  Formal Treatment},
  institution	= {University of York},
  address	= {Heslington, York YO1 5DD, UK},
  type		= {Computer Science Report},
  number	= {YCS116},
  year		= 1989
}

@TechReport{	  z:burn89,
  author	= {A. Burns and A. J. Wellings},
  title		= {Priority Inheritance and Message Passing Communication: A
		  Formal Treatment},
  institution	= {University of York},
  address	= {Heslington, York YO1 5DD, UK},
  type		= {Computer Science Report},
  number	= {YCS116},
  year		= 1989
}

@TechReport{	  z:burn89b,
  author	= {A. Burns and A. J. Wellings},
  title		= {A Formal Description of {Ada} Tasking in {Z}},
  institution	= {University of York},
  address	= {Heslington, York YO1 5DD, UK},
  type		= {Computer Science Report},
  number	= {YCS122},
  year		= 1989
}

@TechReport{	  z:burn89b,
  author	= {A. Burns and A. J. Wellings},
  title		= {A Formal Description of {Ada} Tasking in {Z}},
  institution	= {University of York},
  address	= {Heslington, York YO1 5DD, UK},
  type		= {Computer Science Report},
  number	= {YCS122},
  year		= 1989
}

@Unpublished{	  z:butl94,
  author	= {M. J. Butler},
  title		= {{Z} Specification of the {X400} Reliable Transfer
		  Service},
  note		= {{\AA}bo Akademi University, Finland},
  url		= {file://ftp.abo.fi//pub/cs/papers/michael/x400.ps.Z},
  year		= 1994
}

@Unpublished{	  z:butl94,
  author	= {M. J. Butler},
  title		= {{Z} Specification of the {X400} Reliable Transfer
		  Service},
  note		= {{\AA}bo Akademi University, Finland},
  url		= {file://ftp.abo.fi//pub/cs/papers/michael/x400.ps.Z},
  year		= 1994
}

@Unpublished{	  z:butl94b,
  author	= {M. J. Butler},
  title		= {Feature Interaction Analysis Using {Z}},
  note		= {{\AA}bo Akademi University, Finland},
  url		= {file://ftp.abo.fi//pub/cs/papers/michael/fiz.ps.Z},
  year		= 1994
}

@Unpublished{	  z:butl94b,
  author	= {M. J. Butler},
  title		= {Feature Interaction Analysis Using {Z}},
  note		= {{\AA}bo Akademi University, Finland},
  url		= {file://ftp.abo.fi//pub/cs/papers/michael/fiz.ps.Z},
  year		= 1994
}

@TechReport{	  z:carr93b,
  author	= {D. Carrington and D. J. Duke and I. J. Hayes and J.
		  Welsh},
  title		= {Deriving Modular Designs from Formal Specifications: The
		  Analysis Phase},
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  type		= {Technical Report},
  number	= {93-13},
  url		= {file://ftp.cs.uq.oz.au/pub/SVRC/techreports/tr93-13.ps.Z},
  other		= {See also \cite{z:carr93}.},
  month		= oct,
  year		= 1993
}

@TechReport{	  z:carr93b,
  author	= {D. Carrington and D. J. Duke and I. J. Hayes and J.
		  Welsh},
  title		= {Deriving Modular Designs from Formal Specifications: The
		  Analysis Phase},
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  type		= {Technical Report},
  number	= {93-13},
  url		= {file://ftp.cs.uq.oz.au/pub/SVRC/techreports/tr93-13.ps.Z},
  other		= {See also \cite{z:carr93}.},
  month		= oct,
  year		= 1993
}

@TechReport{	  z:carr94b,
  author	= {D. Carrington and P. Stocks},
  title		= {A Tale of Two Paradigms: Formal methods and software
		  testing},
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  type		= {Technical Report},
  number	= {94-4},
  url		= {file://ftp.cs.uq.oz.au/pub/SVRC/techreports/tr94-4.ps.Z},
  month		= feb,
  year		= 1994
}

@TechReport{	  z:carr94b,
  author	= {D. Carrington and P. Stocks},
  title		= {A Tale of Two Paradigms: Formal methods and software
		  testing},
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  type		= {Technical Report},
  number	= {94-4},
  url		= {file://ftp.cs.uq.oz.au/pub/SVRC/techreports/tr94-4.ps.Z},
  month		= feb,
  year		= 1994
}

@TechReport{	  z:chen92,
  author	= {A. S. K. Cheng and J. Han and J. Welsh and A. Wood},
  title		= {Providing User-Oriented Support for Software Development
		  by Formal Methods},
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  type		= {Technical Report},
  number	= {92-8},
  url		= {file://ftp.cs.uq.oz.au/pub/SVRC/techreports/tr92-8.ps.Z},
  month		= dec,
  year		= 1992
}

@TechReport{	  z:chen92,
  author	= {A. S. K. Cheng and J. Han and J. Welsh and A. Wood},
  title		= {Providing User-Oriented Support for Software Development
		  by Formal Methods},
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  type		= {Technical Report},
  number	= {92-8},
  url		= {file://ftp.cs.uq.oz.au/pub/SVRC/techreports/tr92-8.ps.Z},
  month		= dec,
  year		= 1992
}

@TechReport{	  z:clar90,
  author	= {S. J. Clarke and A. C. Combes and J. A. McDermid},
  title		= {The Analysis of Safety Arguments in the Specification of a
		  Motor Speed Control Loop},
  institution	= {University of York},
  address	= {Heslington, York YO1 5DD, UK},
  type		= {Computer Science Report},
  number	= {YCS136},
  year		= 1990,
  annote	= {This report describes some timing extensions to Z.}
}

@TechReport{	  z:clar90,
  author	= {S. J. Clarke and A. C. Combes and J. A. McDermid},
  title		= {The Analysis of Safety Arguments in the Specification of a
		  Motor Speed Control Loop},
  institution	= {University of York},
  address	= {Heslington, York YO1 5DD, UK},
  type		= {Computer Science Report},
  number	= {YCS136},
  year		= 1990,
  annote	= {This report describes some timing extensions to Z.}
}

@TechReport{	  z:coom92,
  author	= {A. C. Coombes and J. A. McDermid},
  title		= {Specifying Temporal Requirements for Distributed Real-Time
		  Systems in {Z}},
  institution	= {University of York},
  address	= {Heslington, York YO1 5DD, UK},
  type		= {Computer Science Report},
  number	= {YCS176},
  year		= 1992
}

@TechReport{	  z:coom92,
  author	= {A. C. Coombes and J. A. McDermid},
  title		= {Specifying Temporal Requirements for Distributed Real-Time
		  Systems in {Z}},
  institution	= {University of York},
  address	= {Heslington, York YO1 5DD, UK},
  type		= {Computer Science Report},
  number	= {YCS176},
  year		= 1992
}

@TechReport{	  z:crai91a,
  author	= {I. D. Craig},
  title		= {Formal Specification of {AI} Systems: Four Case Studies},
  institution	= {Department of Computer Science, University of Warwick},
  address	= {Coventry CV4 7AL, UK},
  type		= {Research Report},
  number	= {182},
  month		= {March},
  year		= {1991}
}

@TechReport{	  z:crai91b,
  author	= {I. D. Craig},
  title		= {The Formal Specification of a Blackboard Framework},
  institution	= {Department of Computer Science, University of Warwick},
  address	= {Coventry CV4 7AL, UK},
  type		= {Research Report},
  number	= {181},
  month		= {March},
  year		= {1991}
}

@TechReport{	  z:crox90,
  author	= {S. Croxall and P. Lupton and J. B. Wordsworth},
  title		= {A Formal Specification of the {CPI} Communications},
  institution	= {IBM United Kingdom Laboratories Ltd},
  address	= {Hursley Park, Winchester, Hampshire SO21 2JN, UK},
  type		= {{IBM} Technical Report},
  number	= {TR12.277},
  year		= 1990
}

@TechReport{	  z:crox90,
  author	= {S. Croxall and P. Lupton and J. B. Wordsworth},
  title		= {A Formal Specification of the {CPI} Communications},
  institution	= {IBM United Kingdom Laboratories Ltd},
  address	= {Hursley Park, Winchester, Hampshire SO21 2JN, UK},
  type		= {{IBM} Technical Report},
  number	= {TR12.277},
  year		= 1990
}

@TechReport{	  z:deba93,
  author	= {R. S. M. {de Barros}},
  title		= {Formal Specification of Relational Database Applications:
		  A Method and an Example},
  url		= {file://ftp.dcs.glasgow.ac.uk/pub/users/roberto/repmet.ps},
  type		= {Research report},
  number	= {GE-93-02},
  institution	= {Department of Computing Science, University of Glasgow},
  address	= uk,
  month		= sep,
  year		= 1993
}

@TechReport{	  z:deba93,
  author	= {R. S. M. {de Barros}},
  title		= {Formal Specification of Relational Database Applications:
		  A Method and an Example},
  url		= {file://ftp.dcs.glasgow.ac.uk/pub/users/roberto/repmet.ps},
  type		= {Research report},
  number	= {GE-93-02},
  institution	= {Department of Computing Science, University of Glasgow},
  address	= uk,
  month		= sep,
  year		= 1993
}

@TechReport{	  z:deba94b,
  author	= {R. S. M. {de Barros}},
  title		= {On the Derivation of Relational Database Programs from
		  Formal Specifications},
  url		= {file://ftp.dcs.glasgow.ac.uk/pub/users/roberto/repmap.ps},
  type		= {Research report},
  number	= {GE-94-01},
  institution	= {Department of Computing Science, University of Glasgow},
  address	= uk,
  month		= jul,
  year		= 1994,
  length	= 27,
  annote	= {An extended version of \cite{z:deba94}.}
}

@TechReport{	  z:deba94b,
  author	= {R. S. M. {de Barros}},
  title		= {On the Derivation of Relational Database Programs from
		  Formal Specifications},
  url		= {file://ftp.dcs.glasgow.ac.uk/pub/users/roberto/repmap.ps},
  type		= {Research report},
  number	= {GE-94-01},
  institution	= {Department of Computing Science, University of Glasgow},
  address	= uk,
  month		= jul,
  year		= 1994,
  length	= 27,
  annote	= {An extended version of \cite{z:deba94}.}
}

@TechReport{	  z:deva92,
  author	= {A. M. L. {de Vasconcelos} and J. A. McDermid},
  title		= {Incremental Type-Checking in {Z}},
  institution	= {University of York},
  address	= {Heslington, York YO1 5DD, UK},
  type		= {Computer Science Report},
  number	= {YCS185},
  year		= 1992,
  abstract	= {Over the last decade, formal methods have become
		  progressively more widely used to counteract the problems
		  of software development. Nowadays, a relatively large
		  number of formal methods, or notations, are available and Z
		  is one of the most widely used. However, Z is not so
		  widespread in the industrial community as it is in the
		  academic one. \par The provision of automated tools, such
		  as syntax checkers and type checkers, is essential to the
		  successful application of Z on industrial scale problems.
		  The use of these tools during the software specification
		  phase reduces the possibility of errors, and consequently
		  improves the software quality and productivity.}
}

@TechReport{	  z:deva92,
  author	= {A. M. L. {de Vasconcelos} and J. A. McDermid},
  title		= {Incremental Type-Checking in {Z}},
  institution	= {University of York},
  address	= {Heslington, York YO1 5DD, UK},
  type		= {Computer Science Report},
  number	= {YCS185},
  year		= 1992,
  abstract	= {Over the last decade, formal methods have become
		  progressively more widely used to counteract the problems
		  of software development. Nowadays, a relatively large
		  number of formal methods, or notations, are available and Z
		  is one of the most widely used. However, Z is not so
		  widespread in the industrial community as it is in the
		  academic one. \par The provision of automated tools, such
		  as syntax checkers and type checkers, is essential to the
		  successful application of Z on industrial scale problems.
		  The use of these tools during the software specification
		  phase reduces the possibility of errors, and consequently
		  improves the software quality and productivity.}
}

@Book{		  z:dill90,
  author	= {A. Diller},
  title		= {{Z}: An Introduction to Formal Methods},
  publisher	= {John Wiley \& Sons},
  year		= 1990,
  length	= 332,
  price		= {\pounds19.95},
  isbn		= {0-471-92489-X},
  annote	= {This book offers a comprehensive tutorial to Z from the
		  practical viewpoint. Many natural deduction style proofs
		  are presented and exercises are included. A second edition
		  is now available \cite{z:dill94}.},
  other		= {`The best introductory book on Z yet published.' -- the
		  author!}
}

@TechReport{	  z:dill90b,
  author	= {A. Diller},
  title		= {Specifying Interactive Programs in {Z}},
  institution	= {School of Computer Science, University of Birmingham},
  address	= {Birmingham B15 2TT, UK},
  type		= {Research Report},
  number	= {CSR-90-13},
  month		= aug,
  year		= 1990
}

@TechReport{	  z:dill90b,
  author	= {A. Diller},
  title		= {Specifying Interactive Programs in {Z}},
  institution	= {School of Computer Science, University of Birmingham},
  address	= {Birmingham B15 2TT, UK},
  type		= {Research Report},
  number	= {CSR-90-13},
  month		= aug,
  year		= 1990
}

@TechReport{	  z:dill91,
  author	= {A. Diller},
  title		= {Relating to {Z} Specifications and Programs through
		  {Hoare} Logics},
  institution	= {School of Computer Science, University of Birmingham},
  address	= uk,
  type		= {Research Report},
  number	= {CSR-91-3},
  month		= {April},
  year		= {1991},
  annote	= {Copies available from: Mary Cooper, School of Computer
		  Science, Aston Webb Building, University of Birmingham,
		  Edgbaston, Birmingham, B15 2TT, UK.}
}

@MastersThesis{	  z:dinv88,
  author	= {d'Inverno, M.},
  title		= {Using {Z} to Capture the Essence of a Contract Net},
  year		= {1988},
  school	= {Programming Research Group},
  address	= {Oxford University, UK}
}

@TechReport{	  z:duce86,
  author	= {D. A. Duce},
  title		= {A Simple Example from {GKS} in {Z}},
  institution	= {Informatics Division, Rutherford Appleton Laboratories},
  address	= {Chilton, Didcot, Oxon OX11 0QX, UK},
  number	= {RAL-86-082},
  year		= {1986}
}

@TechReport{	  z:duke86,
  author	= {R. Duke and G. A. Rose},
  title		= {A Complete {Z} Specification of an Interactive Program
		  Editor},
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  type		= {Technical Report},
  number	= 71,
  year		= 1986
}

@TechReport{	  z:duke86,
  author	= {R. Duke and G. A. Rose},
  title		= {A Complete {Z} Specification of an Interactive Program
		  Editor},
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  type		= {Technical Report},
  number	= 71,
  year		= 1986
}

@TechReport{	  z:duke89b,
  author	= {D. J. Duke and R. Duke},
  title		= {A History Model for Classes in {Object-Z}},
  type		= {Technical Report},
  number	= 120,
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  year		= 1989
}

@TechReport{	  z:duke89b,
  author	= {D. J. Duke and R. Duke},
  title		= {A History Model for Classes in {Object-Z}},
  type		= {Technical Report},
  number	= 120,
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  year		= 1989
}

@TechReport{	  z:duke92c,
  author	= {D. J. Duke and M. D. Harrison},
  title		= {Abstract Models for Interaction Objects},
  institution	= {ESPRIT BRA 7040 `Amodeus 2'},
  number	= {WP1},
  month		= {November},
  year		= {1992},
  annote	= {Submitted to Eurographics'93 as ``Abstract Interaction
		  Objects''}
}

@TechReport{	  z:duke92d,
  author	= {D. J. Duke and M. D. Harrison},
  title		= {``Synergistic'' Interactors},
  institution	= {ESPRIT BRA 7040 `Amodeus 2'},
  number	= {WP3},
  month		= {December},
  year		= {1992}
}

@TechReport{	  z:duke93,
  author	= {D. J. Duke and M. D. Harrison},
  title		= {Towards a Theory of Interactors},
  institution	= {ESPRIT BRA 7040 `Amodeus 2'},
  number	= {WP6},
  month		= {February},
  year		= {1993}
}

@TechReport{	  z:fidg93b,
  author	= {C. J. Fidge and P. Kearney and J. Staples},
  title		= {Formally Verified Real-Time Software: an Integrated
		  Development Strategy (Extended Version)},
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  type		= {Technical Report},
  number	= {93-10},
  url		= {file://ftp.cs.uq.oz.au/pub/SVRC/techreports/tr93-10.ps.Z},
  month		= jun,
  year		= 1993
}

@TechReport{	  z:fidg93b,
  author	= {C. J. Fidge and P. Kearney and J. Staples},
  title		= {Formally Verified Real-Time Software: an Integrated
		  Development Strategy (Extended Version)},
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  type		= {Technical Report},
  number	= {93-10},
  url		= {file://ftp.cs.uq.oz.au/pub/SVRC/techreports/tr93-10.ps.Z},
  month		= jun,
  year		= 1993
}

@TechReport{	  z:flin85,
  author	= {L. W. Flinn and I. H. S{\o}rensen},
  title		= {{CAVIAR}: A Case Study in Specification},
  institution	= oucl,
  address	= oxford,
  type		= {Technical Monograph},
  number	= {PRG-48},
  length	= {46},
  month		= {July},
  year		= {1985},
  isbn		= {0-902928-29-5}
}

@InProceedings{	  z:gann86,
  author	= {Gannon, McMullen, Hamlet},
  title		= {Data-Abstraction Implementation, Specification, and
		  Testing},
  booktitle	= {ACM TOPLAS},
  month		= {July},
  year		= {1986}
}

@TechReport{	  z:gogu91,
  author	= {A. J. Alencar and J. A. Goguen},
  title		= {Two examples in {OOZE}},
  institution	= oucl,
  address	= oxford,
  type		= {Technical Report},
  number	= {PRG-TR-25-91},
  length	= 21,
  year		= 1991
}

@TechReport{	  z:gogu91,
  author	= {A. J. Alencar and J. A. Goguen},
  title		= {Two examples in {OOZE}},
  institution	= oucl,
  address	= oxford,
  type		= {Technical Report},
  number	= {PRG-TR-25-91},
  length	= 21,
  year		= 1991
}

@TechReport{	  z:good93,
  author	= {H. S. Goodman},
  title		= {Animating {Z} Specifications in {Haskell} Using a Monad},
  number	= {CSR-93-10},
  institution	= {School of Computer Science, University of Birmingham},
  address	= {Birmingham B15 2TT, UK},
  url		= {file://ftp.cs.bham.ac.uk/pub/tech-reports/1993/CSR-93-10.ps.gz}
		  ,
  month		= nov,
  year		= 1993
}

@TechReport{	  z:good93,
  author	= {H. S. Goodman},
  title		= {Animating {Z} Specifications in {Haskell} Using a Monad},
  number	= {CSR-93-10},
  institution	= {School of Computer Science, University of Birmingham},
  address	= {Birmingham B15 2TT, UK},
  url		= {file://ftp.cs.bham.ac.uk/pub/tech-reports/1993/CSR-93-10.ps.gz}
		  ,
  month		= nov,
  year		= 1993
}

@TechReport{	  z:habr93,
  author	= {H. Habrias and S. Dunne and B. Stoddart},
  title		= {{NIAM} and {Z} Specifications},
  institution	= {Institut de Recherche en Informatique de Nantes},
  address	= {IUT de Nantes, D\'epartement Informatique, 3 rue du
		  Mar\'echal Joffre, 44041 Nantes Cedex 01, France},
  type		= {Rapport de recherche IRIN},
  number	= 32,
  month		= may,
  year		= 1993
}

@TechReport{	  z:habr93,
  author	= {H. Habrias and S. Dunne and B. Stoddart},
  title		= {{NIAM} and {Z} Specifications},
  institution	= {Institut de Recherche en Informatique de Nantes},
  address	= {IUT de Nantes, D\'epartement Informatique, 3 rue du
		  Mar\'echal Joffre, 44041 Nantes Cedex 01, France},
  type		= {Rapport de recherche IRIN},
  number	= 32,
  month		= may,
  year		= 1993
}

@TechReport{	  z:harr88,
  author	= {C. L. Harrold},
  title		= {Formal Specification of a Secure Document Control System
		  for {SMITE}},
  institution	= {RSRE, Ministry of Defence},
  address	= {Malvern, Worcestershire, UK},
  type		= {Report},
  number	= {no.\ 88002},
  month		= feb,
  year		= 1988
}

@TechReport{	  z:harr88,
  author	= {C. L. Harrold},
  title		= {Formal Specification of a Secure Document Control System
		  for {SMITE}},
  institution	= {RSRE, Ministry of Defence},
  address	= {Malvern, Worcestershire, UK},
  type		= {Report},
  number	= {no.\ 88002},
  month		= feb,
  year		= 1988
}

@TechReport{	  z:harw91,
  author	= {W. T. Harwood},
  title		= {Proof Rules for {Balzac}},
  institution	= {Imperial Software Technology},
  address	= {Cambridge, UK},
  type		= {Technical Report},
  number	= {WTH/P7/001},
  year		= 1991
}

@TechReport{	  z:harw91,
  author	= {W. T. Harwood},
  title		= {Proof Rules for {Balzac}},
  institution	= {Imperial Software Technology},
  address	= {Cambridge, UK},
  type		= {Technical Report},
  number	= {WTH/P7/001},
  year		= 1991
}

@TechReport{	  z:harw93,
  author	= {K. Harwood and P. A. Lindsay and R. Matthews},
  title		= {An Approach to Constructing Verified Software},
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  type		= {Technical Report},
  number	= {93-8},
  url		= {file://ftp.cs.uq.oz.au/pub/SVRC/techreports/tr93-8.ps.Z},
  month		= sep,
  year		= 1993
}

@TechReport{	  z:harw93,
  author	= {K. Harwood and P. A. Lindsay and R. Matthews},
  title		= {An Approach to Constructing Verified Software},
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  type		= {Technical Report},
  number	= {93-8},
  url		= {file://ftp.cs.uq.oz.au/pub/SVRC/techreports/tr93-8.ps.Z},
  month		= sep,
  year		= 1993
}

@TechReport{	  z:hass92,
  author	= {W. Hasselbring},
  title		= {A Formal {Z} Specification of {ProSet-Linda}},
  institution	= {University of Essen},
  address	= {Fachbereich Mathematik und Informatik -- Software
		  Engineering, Schuetzenbahn 70, 4300 Essen 1, Germany},
  year		= 1992,
  url		= {file://hp06c.informatik.uni-essen.de/pub/Informatik-Berichte/02-92.ps.Z}
		  
}

@TechReport{	  z:hass92,
  author	= {W. Hasselbring},
  title		= {A Formal {Z} Specification of {ProSet-Linda}},
  institution	= {University of Essen},
  address	= {Fachbereich Mathematik und Informatik -- Software
		  Engineering, Schuetzenbahn 70, 4300 Essen 1, Germany},
  year		= 1992,
  url		= {file://hp06c.informatik.uni-essen.de/pub/Informatik-Berichte/02-92.ps.Z}
		  
}

@InProceedings{	  z:haug90,
  author	= {H. P. Haughton and K. C. Lano},
  title		= {Three Dimensional Maintenance},
  booktitle	= {Fourth Software Maintenance Workshop Notes},
  editor	= {M. Munro and P. Carroll},
  organization	= {Centre for Software Maintenance, Durham, UK},
  location	= {University of Durham, UK, 18--20 September 1990},
  length	= 19,
  month		= {18--20 September},
  year		= 1990,
  annote	= {An object-oriented extension to Z designed to aid software
		  maintenance. is presented}
}

@InProceedings{	  z:haug90,
  author	= {H. P. Haughton and K. C. Lano},
  title		= {Three Dimensional Maintenance},
  booktitle	= {Fourth Software Maintenance Workshop Notes},
  editor	= {M. Munro and P. Carroll},
  organization	= {Centre for Software Maintenance, Durham, UK},
  location	= {University of Durham, UK, 18--20 September 1990},
  length	= 19,
  month		= {18--20 September},
  year		= 1990,
  annote	= {An object-oriented extension to Z designed to aid software
		  maintenance. is presented}
}

@TechReport{	  z:haye90,
  author	= {I. J. Hayes},
  title		= {Specifying Physical Limitations: A Case Study of an
		  Oscilloscope},
  type		= {Technical Report},
  number	= 167,
  length	= 17,
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  month		= jul,
  year		= 1990
}

@TechReport{	  z:haye90,
  author	= {I. J. Hayes},
  title		= {Specifying Physical Limitations: A Case Study of an
		  Oscilloscope},
  type		= {Technical Report},
  number	= 167,
  length	= 17,
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  month		= jul,
  year		= 1990
}

@TechReport{	  z:haye90c,
  author	= {I. J. Hayes},
  title		= {Multi-sets and Multi-relations in {Z} with an Application
		  to a Bill-of-materials System},
  type		= {Technical Report},
  number	= {UQCS-176},
  url		= {file://ftp.cs.uq.oz.au/pub/TECHREPORTS/department/TR0176.ps.Z}
		  ,
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  month		= jul,
  year		= 1990,
  other		= {Printed November 1994},
  annote	= {The first chapter is an updated version of
		  \cite{z:haye90b} and the second and third chapters are
		  updated versions of \cite{z:haye92b}. The changes are
		  mainly for consistency with \cite{z:haye93,z:spiv92}.}
}

@TechReport{	  z:haye90c,
  author	= {I. J. Hayes},
  title		= {Multi-sets and Multi-relations in {Z} with an Application
		  to a Bill-of-materials System},
  type		= {Technical Report},
  number	= {UQCS-176},
  url		= {file://ftp.cs.uq.oz.au/pub/TECHREPORTS/department/TR0176.ps.Z}
		  ,
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  month		= jul,
  year		= 1990,
  other		= {Printed November 1994},
  annote	= {The first chapter is an updated version of
		  \cite{z:haye90b} and the second and third chapters are
		  updated versions of \cite{z:haye92b}. The changes are
		  mainly for consistency with \cite{z:haye93,z:spiv92}.}
}

@TechReport{	  z:hepw90b,
  author	= {B. Hepworth},
  title		= {{ZIP} Project Overview},
  institution	= {Software Technology Department, British Aerospace},
  address	= {Warton PR4 1AX, UK},
  type		= {DTI IED Project No.~1639 Report},
  number	= {ZIP/BAe/90/017},
  edition	= {Issue 2.0},
  month		= {December},
  year		= {1990}
}

@Unpublished{	  z:hewi91,
  author	= {M. A. Hewitt},
  title		= {Automated Animation of {Z} using {Prolog}},
  note		= {B.Sc.\ Project Report, Department of Computing, Lancaster
		  University, UK},
  month		= {August},
  year		= {1991}
}

@Unpublished{	  z:hewi91b,
  author	= {M. A. Hewitt},
  title		= {Optimization of {Prolog} Generated from {Z}
		  Specifications},
  note		= {Department of Computing Science, University of Aberdeen,
		  UK},
  month		= {September},
  year		= {1991},
  annote	= {Copies available from: Mark Hewitt, L115 DRA Malvern, St.\
		  Andrews Road, Great Malvern, Worcestershire WR14 3PS, UK.
		  Telephone: +44-684-895188. Email:
		  \verb"<MAHEWITT%hermes.mod.uk>".}
}

@InProceedings{	  z:hoer93,
  author	= {H.-M. H\"orcher},
  title		= {Formale Spezifikationen zur Auswertung von
		  Testergebnissen},
  editor	= {H. Reichel},
  booktitle	= {Informatik, Wirtschaft, Gesellschaft -- 23.
		  GI-Jahrestagung},
  organization	= {Gesellschaft f\"ur Informatik (GI)},
  publisher	= {Springer-Verlag},
  series	= {Informatik Aktuell},
  month		= {October},
  year		= 1993,
  other		= {Describes typical problems with software testing and how
		  these can be solved by (automatically) evaluating the test
		  results against the specification.}
}

@Article{	  z:hoer94b,
  author	= {Hans-Martin H\"orcher},
  title		= {Animation of Implicit Specifications},
  journal	= {FACS Europe Newsletter},
  year		= {in preparation}
}

@TechReport{	  z:hous90,
  author	= {I. S. C. Houston and J. B. Wordsworth},
  title		= {A {Z} Specification of Part of the {CICS} File Control
		  {API}},
  institution	= {IBM United Kingdom Laboratories Ltd},
  address	= {Hursley Park, Winchester, Hampshire SO21 2JN, UK},
  type		= {{IBM} Technical Report},
  number	= {TR12.272},
  year		= 1990
}

@TechReport{	  z:hous90,
  author	= {I. S. C. Houston and J. B. Wordsworth},
  title		= {A {Z} Specification of Part of the {CICS} File Control
		  {API}},
  institution	= {IBM United Kingdom Laboratories Ltd},
  address	= {Hursley Park, Winchester, Hampshire SO21 2JN, UK},
  type		= {{IBM} Technical Report},
  number	= {TR12.272},
  year		= 1990
}

@TechReport{	  z:hous90b,
  author	= {I. S. C. Houston},
  title		= {The {CICS} Application Programming Interface: Automatic
		  transaction initiation},
  institution	= {IBM United Kingdom Laboratories Ltd},
  address	= {Hursley Park, Winchester, Hampshire SO21 2JN, UK},
  type		= {{IBM} Technical Report},
  number	= {TR12.300},
  edition	= {Version 2.3},
  month		= dec,
  year		= 1990,
  annote	= {One of a number of reports on the CICS application
		  programming interface. See also
		  \cite{z:blyt90,z:king90c,z:mund90}.}
}

@TechReport{	  z:hous90b,
  author	= {I. S. C. Houston},
  title		= {The {CICS} Application Programming Interface: Automatic
		  transaction initiation},
  institution	= {IBM United Kingdom Laboratories Ltd},
  address	= {Hursley Park, Winchester, Hampshire SO21 2JN, UK},
  type		= {{IBM} Technical Report},
  number	= {TR12.300},
  edition	= {Version 2.3},
  month		= dec,
  year		= 1990,
  annote	= {One of a number of reports on the CICS application
		  programming interface. See also
		  \cite{z:blyt90,z:king90c,z:mund90}.}
}

@Book{		  z:ince88,
  author	= {D. C. Ince},
  title		= {An Introduction to Discrete Mathematics and Formal System
		  Specification},
  publisher	= {Oxford University Press},
  address	= uk,
  series	= {Oxford Applied Mathematics and Computing Science Series},
  year		= 1988,
  length	= 349,
  isbn		= {0-19-859667-7},
  price		= {\pounds30.00 or $65.00 hardback},
  annote	= {A second edition is now available.}
}

@TechReport{	  z:jack94,
  author	= {D. Jackson},
  title		= {Structuring {Z} Specifications with Views},
  institution	= {Carnegie-Mellon University},
  address	= {USA},
  type		= {Technical Report},
  number	= {CMU-CS-94-126},
  url		= {file://reports.adm.cs.cmu.edu/1994/CMU-CS-94-126.ps},
  month		= mar,
  year		= 1994
}

@TechReport{	  z:jack94,
  author	= {D. Jackson},
  title		= {Structuring {Z} Specifications with Views},
  institution	= {Carnegie-Mellon University},
  address	= {USA},
  type		= {Technical Report},
  number	= {CMU-CS-94-126},
  url		= {file://reports.adm.cs.cmu.edu/1994/CMU-CS-94-126.ps},
  month		= mar,
  year		= 1994
}

@TechReport{	  z:john93,
  author	= {W. Johnston and G. A. Rose},
  title		= {Guidelines for the Manual Conversion of {Object-Z} to
		  {C++}},
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  type		= {Technical Report},
  number	= {93-14},
  url		= {file://ftp.cs.uq.oz.au/pub/SVRC/techreports/tr93-14.ps.Z},
  month		= sep,
  year		= 1993
}

@TechReport{	  z:john93,
  author	= {W. Johnston and G. A. Rose},
  title		= {Guidelines for the Manual Conversion of {Object-Z} to
		  {C++}},
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  type		= {Technical Report},
  number	= {93-14},
  url		= {file://ftp.cs.uq.oz.au/pub/SVRC/techreports/tr93-14.ps.Z},
  month		= sep,
  year		= 1993
}

@TechReport{	  z:jord91b,
  author	= {L. E. Jordan},
  title		= {The Kernel {Z} Type Checking Rules},
  institution	= {Imperial Software Technology},
  address	= {Cambridge, UK},
  type		= {Technical Report},
  number	= {LEJ/\-TC3/\-001},
  year		= 1991
}

@TechReport{	  z:jord91b,
  author	= {L. E. Jordan},
  title		= {The Kernel {Z} Type Checking Rules},
  institution	= {Imperial Software Technology},
  address	= {Cambridge, UK},
  type		= {Technical Report},
  number	= {LEJ/\-TC3/\-001},
  year		= 1991
}

@TechReport{	  z:jord91c,
  author	= {L. E. Jordan},
  title		= {The {Z} Syntax Supported by {Balzac-II/1}},
  institution	= {Imperial Software Technology},
  address	= {Cambridge, UK},
  type		= {Technical Report},
  number	= {LEJ/\-S1/\-001},
  year		= 1991
}

@TechReport{	  z:jord91c,
  author	= {L. E. Jordan},
  title		= {The {Z} Syntax Supported by {Balzac-II/1}},
  institution	= {Imperial Software Technology},
  address	= {Cambridge, UK},
  type		= {Technical Report},
  number	= {LEJ/\-S1/\-001},
  year		= 1991
}

@TechReport{	  z:jose91,
  author	= {M. B. Josephs},
  title		= {Specifying Reactive Systems in {Z}},
  institution	= oucl,
  address	= oxford,
  type		= {Technical Report},
  number	= {PRG-TR-19-91},
  length	= 9,
  month		= jul,
  year		= 1991
}

@TechReport{	  z:jose91,
  author	= {M. B. Josephs},
  title		= {Specifying Reactive Systems in {Z}},
  institution	= oucl,
  address	= oxford,
  type		= {Technical Report},
  number	= {PRG-TR-19-91},
  length	= 9,
  month		= jul,
  year		= 1991
}

@TechReport{	  z:jose91b,
  author	= {M. B. Josephs and D. Redmond-Pyle},
  title		= {Entity-Relationship Models Expressed in {Z}: A Synthesis
		  of Structured and Formal Methods},
  institution	= oucl,
  address	= oxford,
  type		= {Technical Report},
  number	= {PRG-TR-20-91},
  length	= 15,
  month		= jul,
  year		= 1991
}

@TechReport{	  z:jose91b,
  author	= {M. B. Josephs and D. Redmond-Pyle},
  title		= {Entity-Relationship Models Expressed in {Z}: A Synthesis
		  of Structured and Formal Methods},
  institution	= oucl,
  address	= oxford,
  type		= {Technical Report},
  number	= {PRG-TR-20-91},
  length	= 15,
  month		= jul,
  year		= 1991
}

@TechReport{	  z:jose91c,
  author	= {M. B. Josephs and D. Redmond-Pyle},
  title		= {A Library of {Z} Schemas for use in Entity-Relationship
		  Modelling},
  institution	= oucl,
  address	= oxford,
  type		= {Technical Report},
  number	= {PRG-TR-21-91},
  length	= 6,
  month		= aug,
  year		= 1991
}

@TechReport{	  z:jose91c,
  author	= {M. B. Josephs and D. Redmond-Pyle},
  title		= {A Library of {Z} Schemas for use in Entity-Relationship
		  Modelling},
  institution	= oucl,
  address	= oxford,
  type		= {Technical Report},
  number	= {PRG-TR-21-91},
  length	= 6,
  month		= aug,
  year		= 1991
}

@TechReport{	  z:kemp88,
  author	= {D. H. Kemp},
  title		= {Specification of {Viper1} in {Z}},
  institution	= {RSRE, Ministry of Defence},
  address	= {Malvern, Worcestershire, UK},
  type		= {Memorandum},
  number	= {no.\ 4195},
  length	= 33,
  month		= oct,
  year		= 1988
}

@TechReport{	  z:kemp88,
  author	= {D. H. Kemp},
  title		= {Specification of {Viper1} in {Z}},
  institution	= {RSRE, Ministry of Defence},
  address	= {Malvern, Worcestershire, UK},
  type		= {Memorandum},
  number	= {no.\ 4195},
  length	= 33,
  month		= oct,
  year		= 1988
}

@TechReport{	  z:kemp88b,
  author	= {D. H. Kemp},
  title		= {Specification of {Viper2} in {Z}},
  institution	= {RSRE, Ministry of Defence},
  address	= {Malvern, Worcestershire, UK},
  type		= {Memorandum},
  number	= {no.\ 4217},
  length	= 64,
  month		= oct,
  year		= 1988
}

@TechReport{	  z:kemp88b,
  author	= {D. H. Kemp},
  title		= {Specification of {Viper2} in {Z}},
  institution	= {RSRE, Ministry of Defence},
  address	= {Malvern, Worcestershire, UK},
  type		= {Memorandum},
  number	= {no.\ 4217},
  length	= 64,
  month		= oct,
  year		= 1988
}

@TechReport{	  z:king90c,
  author	= {S. King},
  title		= {The {CICS} Application Programming Interface: Program
		  control},
  institution	= {IBM United Kingdom Laboratories Ltd},
  address	= {Hursley Park, Winchester, Hampshire SO21 2JN, UK},
  type		= {{IBM} Technical Report},
  number	= {TR12.302},
  edition	= {Version 0.3},
  month		= dec,
  year		= 1990,
  annote	= {One of a number of reports on the CICS application
		  programming interface. See also
		  \cite{z:blyt90,z:hous90b,z:mund90}.}
}

@TechReport{	  z:king90c,
  author	= {S. King},
  title		= {The {CICS} Application Programming Interface: Program
		  control},
  institution	= {IBM United Kingdom Laboratories Ltd},
  address	= {Hursley Park, Winchester, Hampshire SO21 2JN, UK},
  type		= {{IBM} Technical Report},
  number	= {TR12.302},
  edition	= {Version 0.3},
  month		= dec,
  year		= 1990,
  annote	= {One of a number of reports on the CICS application
		  programming interface. See also
		  \cite{z:blyt90,z:hous90b,z:mund90}.}
}

@TechReport{	  z:knag91,
  editor	= {P. Knaggs},
  author	= {P. Knaggs},
  title		= {Formal Descriptive Languages (Student Reports), {MSc
		  Software Engineering} 1990/91},
  institution	= {School of Computing and Mathematics, Teesside
		  Polytechnic},
  address	= {Middlesbrough, Cleveland TS1 3BA, UK},
  year		= 1991,
  annote	= {This is a collection of reports, written by the students
		  on the MSc in Software Engineering course. These reports
		  were written after a 20 hour introduction to Z and were
		  collected and produced by Peter Knaggs.}
}

@PhDThesis{	  z:knag93,
  author	= {P. J. Knaggs},
  title		= {Software development techniques for multi-processor {RISC}
		  target machines},
  school	= {School of Compuring and Mathematics, University of
		  Teesside},
  type		= {Ph.D.\ Thesis},
  address	= {Borough Road, Middlesbrough, Cleveland TS1 3BA, UK},
  month		= {March},
  year		= 1993,
  other		= {This work is currently under consideration for the award
		  of Ph.D.}
}

@TechReport{	  z:knot88,
  author	= {R. D. Knott and P. J. Krause},
  title		= {An Approach to Animating {Z} using {Prolog}},
  institution	= {Department of Mathematics, University of Surrey},
  address	= uk,
  type		= {Alvey Project SE/065 report},
  number	= {A1.1},
  year		= {1988}
}

@TechReport{	  z:knot88b,
  author	= {R. D. Knott and P. J. Krause},
  title		= {An Example of the Rapid Prototyping of a {Z} Specification
		  in {Prolog}},
  institution	= {Department of Mathematics, University of Surrey},
  address	= uk,
  type		= {Alvey Project SE/065 report},
  number	= {A1.2},
  year		= {1988}
}

@TechReport{	  z:knot88c,
  author	= {R. D. Knott and P. J. Krause},
  title		= {On the Derivation of an Effective Animation: Telephone
		  Network Case Study},
  institution	= {Department of Mathematics, University of Surrey},
  address	= uk,
  type		= {Alvey Project SE/065 report},
  number	= {A1.3},
  year		= {1988}
}

@TechReport{	  z:lai91,
  author	= {M. K. F. Lai},
  title		= {A Formal Interpretation of the {MAA} Standard in {Z}},
  institution	= {National Physical Laboratory},
  address	= {Teddington, Middlesex, UK},
  series	= {NPL Report},
  number	= {DITC 184/91},
  month		= jun,
  year		= 1991
}

@TechReport{	  z:lai91,
  author	= {M. K. F. Lai},
  title		= {A Formal Interpretation of the {MAA} Standard in {Z}},
  institution	= {National Physical Laboratory},
  address	= {Teddington, Middlesex, UK},
  series	= {NPL Report},
  number	= {DITC 184/91},
  month		= jun,
  year		= 1991
}

@TechReport{	  z:lano91b,
  author	= {K. C. Lano and H. P. Haughton and P. T. Breuer},
  title		= {Using Object-oriented Extensions of {Z} for Maintenance
		  and Reverse-engineering},
  institution	= oucl,
  address	= oxford,
  type		= {Technical Report},
  number	= {PRG-TR-22-91},
  length	= 78,
  year		= 1991
}

@TechReport{	  z:lano91b,
  author	= {K. C. Lano and H. P. Haughton and P. T. Breuer},
  title		= {Using Object-oriented Extensions of {Z} for Maintenance
		  and Reverse-engineering},
  institution	= oucl,
  address	= oxford,
  type		= {Technical Report},
  number	= {PRG-TR-22-91},
  length	= 78,
  year		= 1991
}

@TechReport{	  z:lind93,
  author	= {P. A. Lindsay},
  title		= {Reasoning about {Z} Specifications: A {VDM} Perspective},
  type		= {Technical Report},
  number	= {93-20},
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  url		= {file://ftp.cs.uq.oz.au/pub/SVRC/techreports/tr93-20.ps.Z},
  month		= oct,
  year		= 1993
}

@TechReport{	  z:lind93,
  author	= {P. A. Lindsay},
  title		= {Reasoning about {Z} Specifications: A {VDM} Perspective},
  type		= {Technical Report},
  number	= {93-20},
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  url		= {file://ftp.cs.uq.oz.au/pub/SVRC/techreports/tr93-20.ps.Z},
  month		= oct,
  year		= 1993
}

@TechReport{	  z:lind94b,
  author	= {P. A. Lindsay and E. {van Keulen}},
  title		= {Case Studies in the Verification of Specifications in
		  {VDM} and {Z}},
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  type		= {Technical Report},
  number	= {94-3},
  url		= {file://ftp.cs.uq.oz.au/pub/SVRC/techreports/tr94-3.ps.Z},
  month		= mar,
  year		= 1994
}

@TechReport{	  z:lind94b,
  author	= {P. A. Lindsay and E. {van Keulen}},
  title		= {Case Studies in the Verification of Specifications in
		  {VDM} and {Z}},
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  type		= {Technical Report},
  number	= {94-3},
  url		= {file://ftp.cs.uq.oz.au/pub/SVRC/techreports/tr94-3.ps.Z},
  month		= mar,
  year		= 1994
}

@TechReport{	  z:lind95,
  author	= {P.A. Lindsay},
  title		= {A Syntax for System Specification that Integrates {VDM-SL}
		  and {Z}},
  number	= {SVRC-95-11},
  institution	= {Software Verification Research Centre},
  address	= {Department of Computer Science, University of Queensland,
		  St. Lucia, QLD 4072, Australia},
  month		= dec,
  year		= 1995,
  abstract	= {This report defines the {ViZ} syntax for formal
		  specification. {ViZ} aims to provide a simple semantic
		  framework within which {Z} and {VDM-SL} can be integrated.
		  The framework is based on standard techniques from Naive
		  Set Theory, Model Theory and Automata Theory. The report
		  defines the {ViZ} syntax and its static semantics, and
		  outlines the denotational semantics.},
  url		= {http://www.cs.uq.edu.au/cgi-bin/svrc-tech-report?95-11}
}

@TechReport{	  z:lind95,
  author	= {P.A. Lindsay},
  title		= {A Syntax for System Specification that Integrates {VDM-SL}
		  and {Z}},
  number	= {SVRC-95-11},
  institution	= {Software Verification Research Centre},
  address	= {Department of Computer Science, University of Queensland,
		  St. Lucia, QLD 4072, Australia},
  month		= dec,
  year		= 1995,
  abstract	= {This report defines the {ViZ} syntax for formal
		  specification. {ViZ} aims to provide a simple semantic
		  framework within which {Z} and {VDM-SL} can be integrated.
		  The framework is based on standard techniques from Naive
		  Set Theory, Model Theory and Automata Theory. The report
		  defines the {ViZ} syntax and its static semantics, and
		  outlines the denotational semantics.},
  url		= {http://www.cs.uq.edu.au/cgi-bin/svrc-tech-report?95-11}
}

@TechReport{	  z:lond88,
  author	= {R. L. London},
  title		= {Specifying Reusable Components Using {Z}: Sets Implemented
		  by Bit Vectors},
  institution	= {Tektronix Laboratories},
  address	= {P. O. Box 500, MS 50-662, Beaverton, Oregon 97077, USA},
  type		= {Technical Report},
  number	= {CR-88-14},
  month		= nov,
  year		= 1988
}

@TechReport{	  z:lond88,
  author	= {R. L. London},
  title		= {Specifying Reusable Components Using {Z}: Sets Implemented
		  by Bit Vectors},
  institution	= {Tektronix Laboratories},
  address	= {P. O. Box 500, MS 50-662, Beaverton, Oregon 97077, USA},
  type		= {Technical Report},
  number	= {CR-88-14},
  month		= nov,
  year		= 1988
}

@TechReport{	  z:macd93,
  author	= {A. MacDonald and D. Carrington},
  title		= {Synthesising Designs from Formal Specifications: A Case
		  Study},
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  type		= {Technical Report},
  number	= {93-21},
  url		= {file://ftp.cs.uq.oz.au/pub/SVRC/techreports/tr93-21.ps.Z},
  month		= nov,
  year		= 1993
}

@TechReport{	  z:macd93,
  author	= {A. MacDonald and D. Carrington},
  title		= {Synthesising Designs from Formal Specifications: A Case
		  Study},
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  type		= {Technical Report},
  number	= {93-21},
  url		= {file://ftp.cs.uq.oz.au/pub/SVRC/techreports/tr93-21.ps.Z},
  month		= nov,
  year		= 1993
}

@MastersThesis{	  z:maha90,
  author	= {S. Maharaj},
  title		= {Implementing {Z} in {LEGO}},
  school	= {University of Edinburgh},
  address	= {UK},
  year		= 1990
}

@InProceedings{	  z:maha93,
  author	= {S. Maharaj},
  title		= {Encoding {Z} Schemas in Type Theory},
  editor	= {H. Geuves},
  booktitle	= {Informal Proceedings of the 1993 Workshop on Types for
		  Proofs and Programs},
  pages		= {209-218},
  year		= 1993,
  note		= {Distributed electronically}
}

@TechReport{	  z:maho93,
  author	= {B. P. Mahony and C. Millerchip and I. J. Hayes},
  title		= {A Boiler Control System: A Case-Study in Timed
		  Refinement},
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  url		= {file://ftp.cs.uq.oz.au/pub/TECHREPORTS/department/boilerdesign.ps.Z}
		  ,
  annote	= {A specification and top-level design of a steam generating
		  boiler system is presented as an example of the formal
		  development of a real-time system.},
  month		= {23 June},
  year		= 1993
}

@TechReport{	  z:maho93,
  author	= {B. P. Mahony and C. Millerchip and I. J. Hayes},
  title		= {A Boiler Control System: A Case-Study in Timed
		  Refinement},
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  url		= {file://ftp.cs.uq.oz.au/pub/TECHREPORTS/department/boilerdesign.ps.Z}
		  ,
  annote	= {A specification and top-level design of a steam generating
		  boiler system is presented as an example of the formal
		  development of a real-time system.},
  month		= {23 June},
  year		= 1993
}

@InProceedings{	  z:mand93,
  author	= {K. Mander},
  title		= {The {SAZ} Project: Integrating {SSADM} and {Z}},
  booktitle	= {1993 JFIT Technical Conference, Keele University, UK},
  location	= {Keele University, UK, 23--24 March 1993},
  month		= {23--24 March},
  year		= {1993}
}

@TechReport{	  z:mart94,
  author	= {P. Martin},
  title		= {The Formal Specification in {Z} of Task Migration on the
		  Testbed Multicomputer},
  institution	= {Department of Computer Science, University of Edinburgh},
  address	= {Edinburgh EH9 3JZ, UK},
  type		= {Technical Report},
  number	= {ECS-CSG-2-94},
  length	= 69,
  url		= {file://ftp.dcs.ed.ac.uk/pub/pmar/ECS-CSG-2-94.ps.Z},
  month		= feb,
  year		= 1994,
  abstract	= {This report introduces a message-passing multicomputer
		  called the `Testbed' and describes its facilities for
		  transparent task migration between processors. A
		  specification in the formal language Z is given for the key
		  operating system components which support migration.
		  Finally, rigorous arguments are presented which verify that
		  task migration is correct and safe. The contributions of
		  this report are an extended specification showing the
		  application of Z to a real system and a detailed
		  demonstration of the verification of safety and correctness
		  properties. Conclusions are drawn about the utility of
		  formal methods in general.},
  comment	= {To appear in {\em IEEE Software}},
  keywords	= {formal specification, correctness proofs, the Z language,
		  task migration}
}

@TechReport{	  z:mart94,
  author	= {P. Martin},
  title		= {The Formal Specification in {Z} of Task Migration on the
		  Testbed Multicomputer},
  institution	= {Department of Computer Science, University of Edinburgh},
  address	= {Edinburgh EH9 3JZ, UK},
  type		= {Technical Report},
  number	= {ECS-CSG-2-94},
  length	= 69,
  url		= {file://ftp.dcs.ed.ac.uk/pub/pmar/ECS-CSG-2-94.ps.Z},
  month		= feb,
  year		= 1994,
  abstract	= {This report introduces a message-passing multicomputer
		  called the `Testbed' and describes its facilities for
		  transparent task migration between processors. A
		  specification in the formal language Z is given for the key
		  operating system components which support migration.
		  Finally, rigorous arguments are presented which verify that
		  task migration is correct and safe. The contributions of
		  this report are an extended specification showing the
		  application of Z to a real system and a detailed
		  demonstration of the verification of safety and correctness
		  properties. Conclusions are drawn about the utility of
		  formal methods in general.},
  comment	= {To appear in {\em IEEE Software}},
  keywords	= {formal specification, correctness proofs, the Z language,
		  task migration}
}

@Book{		  z:mcde92,
  author	= {J. A. McDermid and P. Whysall},
  title		= {Formal System Specification and Implementation using {Z}},
  publisher	= {Prentice Hall},
  address	= {Hemel Hempstead, Hertfordshire, UK},
  series	= {International Series in Computer Science},
  length	= {500},
  year		= {1992},
  isbn		= {13-326380-0},
  price		= {\pounds18.99 (\$37.00) paperback},
  note		= {Withdrawn},
  annote	= {A comprehensive introduction to the use of Z
		  specifications. The emphasis on the application of Z
		  enables the reader to appreciate how to use it in
		  specifying and developing software systems. Written in a
		  tutorial style, the book: \begin{itemize} \item discussed
		  an approach to large-scale modular specifications using
		  object-oriented techniques; \item includes the development
		  of code from specifications; \item provides a practical
		  engineering treatment of formal specifications; \item deals
		  with the problems of scale and modular specifications;
		  \item embodies up-to-date research results. \end{itemize}}
}

@TechReport{	  z:meir92,
  author	= {S. L. Meira and A. L. C. Cavalcanti},
  title		= {The {MooZ} Specification Language},
  institution	= {Universidade Federal de Pernambuco, Departamento de
		  Inform\'atica},
  address	= {Recife -- PE, Brasil},
  year		= 1992,
  url		= {file://gctc.itep.br/pub/MooZ/MooZ.ps.Z}
}

@TechReport{	  z:meir92,
  author	= {S. L. Meira and A. L. C. Cavalcanti},
  title		= {The {MooZ} Specification Language},
  institution	= {Universidade Federal de Pernambuco, Departamento de
		  Inform\'atica},
  address	= {Recife -- PE, Brasil},
  year		= 1992,
  url		= {file://gctc.itep.br/pub/MooZ/MooZ.ps.Z}
}

@InCollection{	  z:meir93,
  author	= {S. R. L. Meira and A. L. C. Cavalcanti and C. S. Santos},
  title		= {The {Unix} Filing System: A {MooZ} Specification},
  booktitle	= {Object Oriented Specifications Case Studies},
  editor	= {K. C. Lano and H. Haughton},
  publisher	= {Prentice-Hall},
  other		= {Recife -- PE},
  year		= {1993}
}

@MastersThesis{	  z:mikk93,
  author	= {E. Mikk},
  title		= {Automatic Compilation of {Z} Specifications into {C} for
		  automatic Test Result Evaluation},
  school	= {Christian Albrecht Universit\"at Kiel},
  address	= {Germany},
  month		= {December},
  year		= 1993,
  other		= {Describes the implementation of a schema compiler
		  translating Z operations into C pre- and postcondition
		  evaluation functions.}
}

@TechReport{	  z:mund90,
  author	= {P. Mundy and J. B. Wordsworth},
  title		= {The {CICS} Application Programming Interface: Transient
		  data and storage control},
  institution	= {IBM United Kingdom Laboratories Ltd},
  address	= {Hursley Park, Winchester, Hampshire SO21 2JN, UK},
  type		= {{IBM} Technical Report},
  number	= {TR12.299},
  month		= oct,
  year		= 1990,
  annote	= {One of a number of reports on the CICS application
		  programming interface. See also
		  \cite{z:blyt90,z:hous90b,z:king90c}.}
}

@TechReport{	  z:mund90,
  author	= {P. Mundy and J. B. Wordsworth},
  title		= {The {CICS} Application Programming Interface: Transient
		  data and storage control},
  institution	= {IBM United Kingdom Laboratories Ltd},
  address	= {Hursley Park, Winchester, Hampshire SO21 2JN, UK},
  type		= {{IBM} Technical Report},
  number	= {TR12.299},
  month		= oct,
  year		= 1990,
  annote	= {One of a number of reports on the CICS application
		  programming interface. See also
		  \cite{z:blyt90,z:hous90b,z:king90c}.}
}

@InProceedings{	  z:neil87,
  author	= {D. S. Neilson},
  title		= {Hierarchical Refinement of a {Z} Specification},
  booktitle	= {Proc.\ Foundations of Software Technology and Theoretical
		  Computer Science},
  address	= {Pune, India},
  location	= {Pune, India, December 1987},
  month		= {December},
  year		= {1987}
}

@TechReport{	  z:nich91b,
  author	= {J. E. Nicholls},
  title		= {A Survey of {Z} Courses in the {UK}},
  institution	= oucl,
  address	= oxford,
  type		= {Technical Report},
  number	= {PRG-TR-4-91},
  length	= {8},
  month		= {March},
  year		= {1991}
}

@TechReport{	  z:norr86,
  author	= {M. Norris},
  title		= {{Z} -- a Rigorous System Specification Technique},
  institution	= {The National Computing Centre Ltd.},
  address	= {Oxford Road, Manchester M1 7ED, UK},
  type		= {{STARTS} Debrief Report},
  isbn		= {0-85012-583-9},
  year		= {1986},
  telephone	= {+44-61-228-633 or +44-71-353-4875},
  other		= {M. Norris works for British Telecom. The reports are
		  available from: Sales Administration (Publications), NCC
		  Ltd., Oxford Road, Manchester M1 7ED.},
  annote	= {Other reports in the series include: SLIM, PRICE S,
		  ARTEMIS, VDM, SOFCHIP, JSD, SDL, SAFRA and CORE.},
  price		= {\pounds10 each + \pounds1 p\&p for 1st report and 55p for
		  each subsequent report up to a maximum of \pounds4.30.
		  Orders under \pounds100 should be accompanied by a cheque
		  made payable to ``The National Computing Centre Ltd.''.}
}

@TechReport{	  z:ohal87,
  author	= {C. O'Halloran},
  title		= {The Software Repeater (an exercise in {Z} specification)},
  institution	= {RSRE, Ministry of Defence},
  address	= {Malvern, Worcestershire, UK},
  type		= {Report},
  number	= {no.\ 4090},
  year		= 1987
}

@TechReport{	  z:ohal87,
  author	= {C. O'Halloran},
  title		= {The Software Repeater (an exercise in {Z} specification)},
  institution	= {RSRE, Ministry of Defence},
  address	= {Malvern, Worcestershire, UK},
  type		= {Report},
  number	= {no.\ 4090},
  year		= 1987
}

@TechReport{	  z:oxbo88,
  author	= {E. A. Oxborrow and H. M. Ismail},
  title		= {{KBZ} -- An object-oriented approach to the specification
		  and management of knowledge bases},
  institution	= {Computing Laboratory, University of Kent at Canterbury},
  address	= uk,
  type		= {Technical Report},
  number	= {51},
  year		= 1988,
  annote	= {The report describes the important features of KBZ, an
		  extension of Z which should better support the
		  specification of the semantics of conceptual data models.
		  The report then clarifies the use of KBZ by discussing its
		  application in a distributed database environment.}
}

@TechReport{	  z:oxbo88,
  author	= {E. A. Oxborrow and H. M. Ismail},
  title		= {{KBZ} -- An object-oriented approach to the specification
		  and management of knowledge bases},
  institution	= {Computing Laboratory, University of Kent at Canterbury},
  address	= uk,
  type		= {Technical Report},
  number	= {51},
  year		= 1988,
  annote	= {The report describes the important features of KBZ, an
		  extension of Z which should better support the
		  specification of the semantics of conceptual data models.
		  The report then clarifies the use of KBZ by discussing its
		  application in a distributed database environment.}
}

@TechReport{	  z:pele92,
  author	= {J. Peleska},
  title		= {Structured Methods, {Z} and {DST}-{\em f}{\sc uzz}:
		  Provable Correctness for Safety-Critical Software Systems},
  institution	= {DST Deutsche System--Technik GmbH},
  address	= {Kiel, Germany},
  type		= {Internal Report},
  year		= {1992},
  other		= {Describes the combination of Z with structured methods
		  (SA/SD).}
}

@TechReport{	  z:pele92c,
  author	= {J. Peleska},
  title		= {Application of {Z} Specifications for Black Box Testing},
  institution	= {DST Deutsche System--Technik GmbH},
  address	= {Kiel, Germany},
  type		= {Internal Report},
  year		= {1992},
  other		= {Describes how test cases can systematically be drived from
		  a Z specification}
}

@InProceedings{	  z:pele93,
  author	= {J. Peleska},
  title		= {Formale Modellierung der {ITSEC} Funktionalit\"atsklassen},
  editor	= {H. Reichel},
  booktitle	= {Informatik, Wirtschaft, Gesellschaft -- 23.
		  GI-Jahrestagung},
  organization	= {Gesellschaft f\"ur Informatik (GI)},
  publisher	= {Springer-Verlag},
  series	= {Informatik Aktuell},
  month		= {October},
  year		= 1993,
  other		= {Contains a simple modelling of the ITSEC functionality
		  classes using Z. English version (revised) available from
		  the author}
}

@TechReport{	  z:plac90,
  author	= {P. R. H. Place and W. Wood},
  title		= {Survey of Formal Specification Techniques for Reactive
		  Systems},
  type		= {CMU Technical Report},
  number	= {CMU/SEI-90-TR-5, ADA22374},
  institution	= {Software Engineering Institute, Carnegie-Mellon
		  University},
  address	= {Pittsburgh, Pennsylvania 15213, USA},
  year		= 1990
}

@TechReport{	  z:plac90,
  author	= {P. R. H. Place and W. Wood},
  title		= {Survey of Formal Specification Techniques for Reactive
		  Systems},
  type		= {CMU Technical Report},
  number	= {CMU/SEI-90-TR-5, ADA22374},
  institution	= {Software Engineering Institute, Carnegie-Mellon
		  University},
  address	= {Pittsburgh, Pennsylvania 15213, USA},
  year		= 1990
}

@TechReport{	  z:plac91,
  author	= {P. R. H. Place and W. Wood},
  title		= {Formal Development of {Ada} Programs using {Z} and {Anna}:
		  A Case Study},
  type		= {CMU Technical Report},
  institution	= {Software Engineering Institute, Carnegie-Mellon
		  University},
  address	= {Pittsburgh, Pennsylvania 15213, USA},
  number	= {CMU/SEI-91-TR-1, ADA235698},
  month		= feb,
  year		= 1991,
  annote	= {Copies available from: Research Access Inc., 3400 Forbes
		  Avenue, Suite 302, Pittsburgh, PA 15213, USA.},
  telephone	= {+1-800-685-6510, fax: +1-412-682-6530},
  abstract	= {This report describes a method for the formal development
		  of Ada programs from a formal specification written in Z.
		  ANNotated Ada (Anna) is used as an intermediate language
		  linking the more abstract Z specifications to the concrete
		  Ada program. The method relies on the notion that
		  successive small transformations of a specification are
		  easier to verify than a few large transformations.
		  Essentially the method uses three notations for the
		  representation of the system: an implementation-independent
		  notation for the specification of the system, an
		  implementation-dependent notation for the representation of
		  a lower level specification of the system, and the
		  implementation language. Z and Anna are outlined briefly
		  and examples of transformations are presented. A simple Z
		  specification has been chosen and the transformations
		  presented in the report are transformations of the Z
		  specification into Anna. Conclusions are drawn about the
		  development method presented.}
}

@TechReport{	  z:plac91,
  author	= {P. R. H. Place and W. Wood},
  title		= {Formal Development of {Ada} Programs using {Z} and {Anna}:
		  A Case Study},
  type		= {CMU Technical Report},
  institution	= {Software Engineering Institute, Carnegie-Mellon
		  University},
  address	= {Pittsburgh, Pennsylvania 15213, USA},
  number	= {CMU/SEI-91-TR-1, ADA235698},
  month		= feb,
  year		= 1991,
  annote	= {Copies available from: Research Access Inc., 3400 Forbes
		  Avenue, Suite 302, Pittsburgh, PA 15213, USA.},
  telephone	= {+1-800-685-6510, fax: +1-412-682-6530},
  abstract	= {This report describes a method for the formal development
		  of Ada programs from a formal specification written in Z.
		  ANNotated Ada (Anna) is used as an intermediate language
		  linking the more abstract Z specifications to the concrete
		  Ada program. The method relies on the notion that
		  successive small transformations of a specification are
		  easier to verify than a few large transformations.
		  Essentially the method uses three notations for the
		  representation of the system: an implementation-independent
		  notation for the specification of the system, an
		  implementation-dependent notation for the representation of
		  a lower level specification of the system, and the
		  implementation language. Z and Anna are outlined briefly
		  and examples of transformations are presented. A simple Z
		  specification has been chosen and the transformations
		  presented in the report are transformations of the Z
		  specification into Anna. Conclusions are drawn about the
		  development method presented.}
}

@TechReport{	  z:plac93,
  author	= {P. R. H. Place and K. C. Kang},
  title		= {Safety-Critical Software: Status Report and Annotated
		  Bibliography},
  number	= {CMU/SEI-92-TR-5 \& ESC-TR-93-182},
  institution	= {Software Engineering Institute, Carnegie-Mellon
		  University},
  address	= {Pittsburgh, Pennsylvania 15213, USA},
  month		= jun,
  year		= 1993
}

@TechReport{	  z:plac93,
  author	= {P. R. H. Place and K. C. Kang},
  title		= {Safety-Critical Software: Status Report and Annotated
		  Bibliography},
  number	= {CMU/SEI-92-TR-5 \& ESC-TR-93-182},
  institution	= {Software Engineering Institute, Carnegie-Mellon
		  University},
  address	= {Pittsburgh, Pennsylvania 15213, USA},
  month		= jun,
  year		= 1993
}

@Book{		  z:pott91,
  author	= {B. F. Potter and J. E. Sinclair and D. Till},
  title		= {An Introduction to Formal Specification and {Z}},
  publisher	= {Prentice Hall International Series in Computer Science},
  year		= 1991,
  length	= 300,
  price		= {\pounds18.95 (\$33.95) paperback},
  isbn		= {0-13-478702-1},
  url		= {http://www.cs.city.ac.uk/bibliography/cs/database?TCU/CS/1990/12}
		  ,
  annote	= {Contents: Formal specification in the context of software
		  engineering; An informal introduction to logic and set
		  theory; A first specification; The Z notation: the
		  mathematical language, relations and functions, schemas and
		  specification structure; A first specification revisited;
		  Formal reasoning; From specification to program: data and
		  operation refinement, operation decomposition; From theory
		  to practice.}
}

@Book{		  z:pott91,
  author	= {B. F. Potter and J. E. Sinclair and D. Till},
  title		= {An Introduction to Formal Specification and {Z}},
  publisher	= {Prentice Hall International Series in Computer Science},
  year		= 1991,
  length	= 300,
  price		= {\pounds18.95 (\$33.95) paperback},
  isbn		= {0-13-478702-1},
  url		= {http://www.cs.city.ac.uk/bibliography/cs/database?TCU/CS/1990/12}
		  ,
  annote	= {Contents: Formal specification in the context of software
		  engineering; An informal introduction to logic and set
		  theory; A first specification; The Z notation: the
		  mathematical language, relations and functions, schemas and
		  specification structure; A first specification revisited;
		  Formal reasoning; From specification to program: data and
		  operation refinement, operation decomposition; From theory
		  to practice.}
}

@TechReport{	  z:rand90,
  author	= {G. P. Randell},
  title		= {Translating Data Flow Diagrams into {Z} (and vice versa)},
  institution	= {RSRE, Ministry of Defence},
  address	= {Malvern, Worcestershire, UK},
  type		= {Report},
  number	= {no.\ 90019},
  month		= oct,
  year		= 1990
}

@TechReport{	  z:rand90,
  author	= {G. P. Randell},
  title		= {Translating Data Flow Diagrams into {Z} (and vice versa)},
  institution	= {RSRE, Ministry of Defence},
  address	= {Malvern, Worcestershire, UK},
  type		= {Report},
  number	= {no.\ 90019},
  month		= oct,
  year		= 1990
}

@TechReport{	  z:rand92,
  author	= {G. P. Randell},
  title		= {Improving the translation from Data Flow Diagrams into {Z}
		  by incorporating the Data Dictionary},
  institution	= {RSRE, Ministry of Defence},
  address	= {Malvern, Worcestershire, UK},
  type		= {Report},
  number	= {no.\ 92004},
  month		= jan,
  year		= 1992
}

@TechReport{	  z:rand92,
  author	= {G. P. Randell},
  title		= {Improving the translation from Data Flow Diagrams into {Z}
		  by incorporating the Data Dictionary},
  institution	= {RSRE, Ministry of Defence},
  address	= {Malvern, Worcestershire, UK},
  type		= {Report},
  number	= {no.\ 92004},
  month		= jan,
  year		= 1992
}

@TechReport{	  z:raym90,
  author	= {K. Raymond and P. Stocks and D. Carrington},
  title		= {Using {Z} to Specify Distributed Systems},
  institution	= {Key Centre for Software Technology, University of
		  Queensland},
  address	= {St.\ Lucia 4072, Australia},
  type		= {Technical Report},
  number	= 181,
  year		= 1990
}

@TechReport{	  z:raym90,
  author	= {K. Raymond and P. Stocks and D. Carrington},
  title		= {Using {Z} to Specify Distributed Systems},
  institution	= {Key Centre for Software Technology, University of
		  Queensland},
  address	= {St.\ Lucia 4072, Australia},
  type		= {Technical Report},
  number	= 181,
  year		= 1990
}

@TechReport{	  z:ross93,
  author	= {K. J. Ross and P. A. Lindsay},
  title		= {Maintaining Consistency Under Changes to Formal
		  Specifications},
  type		= {Technical Report},
  number	= {93-3},
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  url		= {file://ftp.cs.uq.oz.au/pub/SVRC/techreports/tr93-3.ps.Z},
  month		= mar,
  year		= 1993
}

@TechReport{	  z:ross93,
  author	= {K. J. Ross and P. A. Lindsay},
  title		= {Maintaining Consistency Under Changes to Formal
		  Specifications},
  type		= {Technical Report},
  number	= {93-3},
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  url		= {file://ftp.cs.uq.oz.au/pub/SVRC/techreports/tr93-3.ps.Z},
  month		= mar,
  year		= 1993
}

@TechReport{	  z:saal91,
  author	= {M. Saaltink},
  title		= {{Z} and {EVES}},
  institution	= {Odyssey Research Associates},
  address	= {265 Carling Avenue, Suite 506, Ottawa, Ontario K1S 2E1,
		  Canada},
  type		= {Technical Report},
  number	= {TR-91-5449-02},
  month		= {October},
  year		= {1991},
  annote	= {This is a longer version of \cite{z:saal92} and presents
		  an account of the mechanization of the Z toolkit using the
		  EVES proof system \cite{z:crai91}.}
}

@TechReport{	  z:semm90,
  author	= {L. T. Semmens and P. M. Allen},
  title		= {Using Entity Relationship Models as a Basis for {Z}
		  Specifications},
  institution	= {Leeds Polytechnic, Faculty of Information and Engineering
		  Systems},
  address	= {Leeds, UK},
  type		= {Technical Report},
  number	= {IES1/90},
  year		= 1990
}

@TechReport{	  z:semm90,
  author	= {L. T. Semmens and P. M. Allen},
  title		= {Using Entity Relationship Models as a Basis for {Z}
		  Specifications},
  institution	= {Leeds Polytechnic, Faculty of Information and Engineering
		  Systems},
  address	= {Leeds, UK},
  type		= {Technical Report},
  number	= {IES1/90},
  year		= 1990
}

@TechReport{	  z:semm90b,
  author	= {L. T. Semmens and P. M. Allen},
  title		= {Using {Yourdon} and {Z} to Specify Computer Security: A
		  Case Study},
  institution	= {Leeds Polytechnic, Faculty of Information and Engineering
		  Systems},
  address	= {Leeds, UK},
  type		= {Technical Report},
  number	= {IES4/90},
  year		= 1990
}

@TechReport{	  z:semm90b,
  author	= {L. T. Semmens and P. M. Allen},
  title		= {Using {Yourdon} and {Z} to Specify Computer Security: A
		  Case Study},
  institution	= {Leeds Polytechnic, Faculty of Information and Engineering
		  Systems},
  address	= {Leeds, UK},
  type		= {Technical Report},
  number	= {IES4/90},
  year		= 1990
}

@TechReport{	  z:senn87,
  author	= {C. T. Sennett},
  title		= {A Combined Security and Integrity Policy Model: Appendix
		  to Development Environment for Secure Software},
  institution	= {RSRE, Ministry of Defence},
  address	= {Malvern, Worcestershire, UK},
  type		= {Report},
  number	= {no.\ 87015},
  month		= {November},
  year		= {1987}
}

@TechReport{	  z:senn87b,
  author	= {C. T. Sennett},
  title		= {Review of Type Checking and Scope Rules of the
		  Specification Language {Z}},
  institution	= {RSRE, Ministry of Defence},
  address	= {Malvern, Worcestershire, UK},
  type		= {Report},
  number	= {no.\ 87017},
  month		= nov,
  year		= 1987
}

@TechReport{	  z:senn87b,
  author	= {C. T. Sennett},
  title		= {Review of Type Checking and Scope Rules of the
		  Specification Language {Z}},
  institution	= {RSRE, Ministry of Defence},
  address	= {Malvern, Worcestershire, UK},
  type		= {Report},
  number	= {no.\ 87017},
  month		= nov,
  year		= 1987
}

@TechReport{	  z:senn87c,
  author	= {C. T. Sennett and R. Macdonald},
  title		= {Separability and Security Models},
  institution	= {RSRE, Ministry of Defence},
  address	= {Malvern, Worcestershire, UK},
  type		= {Report},
  number	= {no.\ 87020},
  month		= nov,
  year		= 1987
}

@TechReport{	  z:senn87c,
  author	= {C. T. Sennett and R. Macdonald},
  title		= {Separability and Security Models},
  institution	= {RSRE, Ministry of Defence},
  address	= {Malvern, Worcestershire, UK},
  type		= {Report},
  number	= {no.\ 87020},
  month		= nov,
  year		= 1987
}

@TechReport{	  z:simc89,
  author	= {L. N. Simcox},
  title		= {The Application of {Z} to the Specification of Air Traffic
		  Control Systems: 1},
  institution	= {RSRE, Ministry of Defence},
  address	= {Malvern, Worcestershire, UK},
  type		= {Memorandum},
  number	= {no.\ 4280},
  month		= apr,
  year		= 1989
}

@TechReport{	  z:simc89,
  author	= {L. N. Simcox},
  title		= {The Application of {Z} to the Specification of Air Traffic
		  Control Systems: 1},
  institution	= {RSRE, Ministry of Defence},
  address	= {Malvern, Worcestershire, UK},
  type		= {Memorandum},
  number	= {no.\ 4280},
  month		= apr,
  year		= 1989
}

@TechReport{	  z:smit89b,
  author	= {G. Smith and R. Duke},
  title		= {Specification and Verification of a Cache Coherence
		  Protocol},
  type		= {Technical Report},
  number	= 126,
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  year		= 1989
}

@TechReport{	  z:smit89b,
  author	= {G. Smith and R. Duke},
  title		= {Specification and Verification of a Cache Coherence
		  Protocol},
  type		= {Technical Report},
  number	= 126,
  institution	= {Department of Computer Science, University of Queensland},
  address	= {St.\ Lucia 4072, Australia},
  year		= 1989
}

@TechReport{	  z:smit91,
  author	= {A. Smith},
  title		= {On Recursive Free Types in {Z}},
  institution	= {RSRE, Ministry of Defence},
  address	= {Malvern, Worcestershire, UK},
  type		= {Memorandum},
  number	= {no.\ 91028},
  year		= {1991}
}

@Book{		  z:spiv89,
  author	= {J. M. Spivey},
  title		= {The {Z} Notation: A Reference Manual},
  publisher	= {Prentice Hall},
  address	= {Hemel Hempstead, Hertfordshire, UK},
  series	= {International Series in Computer Science},
  length	= {188},
  year		= {1989},
  isbn		= {0-13-983768-X},
  price		= {\pounds15.95 (\$26.95) paperback},
  annote	= {This book is the first widely available reference manual
		  for the Z notation. See also \cite{z:zip91} for the draft
		  proposed standard and \cite{z:spiv92} for the 2nd edition
		  of this book.}
}

@TechReport{	  z:step92,
  author	= {S. Stepney},
  title		= {Comparative Study of Object Orientation in {Z}},
  institution	= {Logica Cambridge Ltd},
  address	= {Betjeman House, 104 Hills Road, Cambridge CB2 1LQ, UK},
  number	= {ZIP/Logica/90/046, Issue 3.0},
  month		= {November},
  year		= {1990}
}

@Article{	  z:step93b,
  author	= {S. Stepney and R. Barden},
  title		= {Annotated {Z} Bibliography},
  journal	= {Bulletin of the European Association of Theoretical
		  Computer Science},
  volume	= 50,
  pages		= {280-313},
  month		= jun,
  year		= 1993,
  other		= {Superseded by \cite{z:bowe95f}.}
}

@TechReport{	  z:stoc90,
  author	= {P. Stocks and K. Raymond and D. Carrington},
  title		= {Representing Distributed System Concepts in {Z}},
  institution	= {Key Centre for Software Technology, University of
		  Queensland},
  address	= {St.\ Lucia 4072, Australia},
  type		= {Technical Report},
  number	= 180,
  year		= 1990
}

@TechReport{	  z:stoc90,
  author	= {P. Stocks and K. Raymond and D. Carrington},
  title		= {Representing Distributed System Concepts in {Z}},
  institution	= {Key Centre for Software Technology, University of
		  Queensland},
  address	= {St.\ Lucia 4072, Australia},
  type		= {Technical Report},
  number	= 180,
  year		= 1990
}

@TechReport{	  z:terr88,
  author	= {P. F. Terry and S. R. Wiseman},
  title		= {On the Design and Implementation of a Secure Computer
		  System},
  institution	= {RSRE, Ministry of Defence},
  address	= {Malvern, Worcestershire, UK},
  type		= {Memorandum},
  number	= {no.\ 4188},
  month		= jun,
  year		= 1988
}

@TechReport{	  z:terr88,
  author	= {P. F. Terry and S. R. Wiseman},
  title		= {On the Design and Implementation of a Secure Computer
		  System},
  institution	= {RSRE, Ministry of Defence},
  address	= {Malvern, Worcestershire, UK},
  type		= {Memorandum},
  number	= {no.\ 4188},
  month		= jun,
  year		= 1988
}

@Manual{	  z:toyn90,
  author	= {I. Toyn},
  title		= {{CADiZ} Quick Reference Guide},
  organization	= {York Software Engineering Ltd},
  address	= {University of York, UK},
  year		= 1990,
  url		= {http://www.cse-euro.demon.co.uk/yse/products/cadiz/},
  annote	= {A guide to the CADiZ (Computer Aided Design in Z) toolkit.
		  See also \cite{z:jord91} for a paper introducing CADiZ.
		  CADiZ originally used the Unix {\em troff\/} family of text
		  formatting tools, but support for \LaTeX\ \cite{z:lamp93}
		  and MS Word is now available.},
  email		= {yse@cse-euro.demon.co.uk}
}

@TechReport{	  z:toyn93,
  author	= {I. Toyn and A. J. Dix},
  title		= {Efficient Binary Transfer of Pointer Structures},
  type		= {Technical Document},
  institution	= {Computer Science Department, University of York},
  url		= {file://minster.york.ac.uk/hise_reports/cadiz/README
		  bio.ps.Z},
  address	= {York YO1 5DD, UK},
  length	= 20,
  month		= nov,
  year		= {1993}
}

@TechReport{	  z:toyn93,
  author	= {I. Toyn and A. J. Dix},
  title		= {Efficient Binary Transfer of Pointer Structures},
  type		= {Technical Document},
  institution	= {Computer Science Department, University of York},
  url		= {file://minster.york.ac.uk/hise_reports/cadiz/README
		  bio.ps.Z},
  address	= {York YO1 5DD, UK},
  length	= 20,
  month		= nov,
  year		= {1993}
}

@TechReport{	  z:toyn93b,
  author	= {I. Toyn and J. A. McDermid},
  title		= {{CADiZ}: An Architecture for {Z} Tools and its
		  Implementation},
  type		= {Technical Document},
  institution	= {Department of Computer Science, University of York},
  address	= {York YO1 5DD, UK},
  url		= {ftp://minster.york.ac.uk/hise_reports/cadiz/cadiz.ps.Z},
  length	= 26,
  month		= nov,
  year		= 1993
}

@TechReport{	  z:vale93b,
  author	= {S. H. Valentine},
  title		= {Enhancements to the {Z} Mathematical Toolkit},
  institution	= {Dept.\ of Computer Science, University of Brighton, UK},
  year		= {1993}
}

@TechReport{	  z:wise88,
  author	= {S. R. Wiseman and C. L. Harrold},
  title		= {A Security Model and its Implementation},
  institution	= {RSRE, Ministry of Defence},
  address	= {Malvern, Worcestershire, UK},
  type		= {Memorandum},
  number	= {no.\ 4222},
  month		= sep,
  year		= 1988
}

@TechReport{	  z:wise88,
  author	= {S. R. Wiseman and C. L. Harrold},
  title		= {A Security Model and its Implementation},
  institution	= {RSRE, Ministry of Defence},
  address	= {Malvern, Worcestershire, UK},
  type		= {Memorandum},
  number	= {no.\ 4222},
  month		= sep,
  year		= 1988
}

@TechReport{	  z:wood88,
  author	= {A. W. Wood},
  title		= {A {Z} Specification of the {MaCHO} Interface Editor},
  institution	= {RSRE, Ministry of Defence},
  address	= {Malvern, Worcestershire, UK},
  type		= {Memorandum},
  number	= {no.\ 4247},
  month		= nov,
  year		= 1988
}

@TechReport{	  z:wood88,
  author	= {A. W. Wood},
  title		= {A {Z} Specification of the {MaCHO} Interface Editor},
  institution	= {RSRE, Ministry of Defence},
  address	= {Malvern, Worcestershire, UK},
  type		= {Memorandum},
  number	= {no.\ 4247},
  month		= nov,
  year		= 1988
}

@InProceedings{	  z:wood89e,
  author	= {J. C. P. Woodcock},
  title		= {Parallel Refinement in {Z}},
  booktitle	= {Proc.\ Workshop on Refinement},
  location	= {Open University, Milton Keynes, UK, January 1989},
  length	= 12,
  month		= jan,
  year		= 1989
}

@InProceedings{	  z:wood89e,
  author	= {J. C. P. Woodcock},
  title		= {Parallel Refinement in {Z}},
  booktitle	= {Proc.\ Workshop on Refinement},
  location	= {Open University, Milton Keynes, UK, January 1989},
  length	= 12,
  month		= jan,
  year		= 1989
}

@InProceedings{	  z:wood89f,
  author	= {J. C. P. Woodcock},
  title		= {Transaction Refinement in {Z}},
  booktitle	= {Proc.\ Workshop on Refinement},
  location	= {Open University, Milton Keynes, UK, January 1989},
  length	= 6,
  month		= jan,
  year		= 1989
}

@InProceedings{	  z:wood89f,
  author	= {J. C. P. Woodcock},
  title		= {Transaction Refinement in {Z}},
  booktitle	= {Proc.\ Workshop on Refinement},
  location	= {Open University, Milton Keynes, UK, January 1989},
  length	= 6,
  month		= jan,
  year		= 1989
}

@Book{		  z:wood89h,
  author	= {J. C. P. Woodcock and M. Loomes},
  title		= {Software Engineering Mathematics},
  publisher	= {Addison-Wesley Publishing Company},
  length	= 271,
  year		= 1989,
  isbn		= {0-201-50424-3},
  url		= {http://heg-school.aw.com/cseng/authors/woodcock/software/software.html}
		  ,
  annote	= {Also published as: {\em Software Engineering Mathematics:
		  Formal Methods Demystified}, Pitman, 1988.}
}

@Book{		  z:wood89h,
  author	= {J. C. P. Woodcock and M. Loomes},
  title		= {Software Engineering Mathematics},
  publisher	= {Addison-Wesley Publishing Company},
  length	= 271,
  year		= 1989,
  isbn		= {0-201-50424-3},
  url		= {http://heg-school.aw.com/cseng/authors/woodcock/software/software.html}
		  ,
  annote	= {Also published as: {\em Software Engineering Mathematics:
		  Formal Methods Demystified}, Pitman, 1988.}
}

@Book{		  z:wood93,
  author	= {J. C. P. Woodcock},
  title		= {Using Standard {Z}},
  publisher	= {Prentice Hall},
  address	= {Hemel Hempstead, Hertfordshire, UK},
  series	= {International Series in Computer Science},
  year		= {1993},
  note		= {In preparation},
  annote	= {This book covers requirements, specifications and proofs
		  using standard Z. It contains a sound proof system for the
		  entire Z language, and describes in detail the process of
		  finding programs from specifications. The text is supported
		  by many examples and case studies, and has been extensively
		  class tested.}
}

@InProceedings{	  z:word89,
  author	= {J. B. Wordsworth},
  title		= {A {Z} Development Method},
  booktitle	= {Proc.\ Workshop on Refinement},
  location	= {Open University, Milton Keynes, UK, January 1989},
  length	= 30,
  month		= jan,
  year		= 1989
}

@InProceedings{	  z:word89,
  author	= {J. B. Wordsworth},
  title		= {A {Z} Development Method},
  booktitle	= {Proc.\ Workshop on Refinement},
  location	= {Open University, Milton Keynes, UK, January 1989},
  length	= 30,
  month		= jan,
  year		= 1989
}

@InProceedings{	  z:word89b,
  author	= {J. B. Wordsworth},
  title		= {Refinement Tutorial: A Storage Manager},
  booktitle	= {Proc.\ Workshop on Refinement},
  location	= {Open University, Milton Keynes, UK, January 1989},
  length	= 27,
  month		= jan,
  year		= 1989
}

@InProceedings{	  z:word89b,
  author	= {J. B. Wordsworth},
  title		= {Refinement Tutorial: A Storage Manager},
  booktitle	= {Proc.\ Workshop on Refinement},
  location	= {Open University, Milton Keynes, UK, January 1989},
  length	= 27,
  month		= jan,
  year		= 1989
}

@Manual{	  z:xiao94,
  author	= {{Xiaoping Jia}},
  title		= {ZTC: A Type Checker for Z -- User's Guide},
  organization	= {Institute for Software Engineering, Department of Computer
		  Science and Information Systems, DePaul University},
  address	= {Chicago, IL 60604, USA (E-mail: \verb"jia@cs.depaul.edu")},
  length	= 54,
  year		= 1994,
  price		= {Free},
  annote	= {ZTC is a type checker for the Z specification language.
		  ZTC accepts two forms of input: \LaTeX\ with \verb"zed"
		  style option and ZSL, an ASCII version of Z. ZTC can also
		  perform translations between the two input forms. This
		  document is intended to serve as both a user's guide and a
		  reference manual for ZTC. ZTC can be obtained via FTP at
		  \verb"ise.cs.depaul.edu" (140.192.32.117) with user name
		  \verb"ftp" and a password of your e-mail address in the
		  file \verb"/ftp/dist/ZTC1.2.tar.Z". Send e-mail to
		  \verb"jia@cs.depaul.edu" for further information.}
}

@Misc{		  z:zfor,
  key		= {ZZforum},
  editor	= {J. P. Bowen},
  title		= {{Z FORUM}},
  howpublished	= {URL: \verb"ftp://ftp.comlab.ox.ac.uk/pub/Zforum/"},
  year		= {1986 onwards},
  note		= {Electronic mailing list: vol.\ 1.1--9 (1986), vol.\ 2.1--4
		  (1987), vol.\ 3.1--7 (1988), vol.\ 4.1--4 (1989), vol.\
		  5.1--3 (1990)},
  url		= {ftp://ftp.comlab.ox.ac.uk/pub/Zforum/},
  annote	= {Z FORUM is an electronic mailing list. It was initiated as
		  an edited newsletter by Ruaridh Macdonald of DRA (formerly
		  RSRE), Malvern, Worcestershire, UK, and is now maintained
		  by Jonathan Bowen at the Oxford University Computing
		  Laboratory. Contributions should be sent to
		  \verb"zforum@comlab.ox.ac.uk". Requests to join or leave
		  the list should be sent to
		  \verb"zforum-request@comlab.ox.ac.uk". Messages are now
		  forwarded to the list directly to ensure timeliness. The
		  list is also gatewayed to the {\sc usenet} newsgroup
		  \verb"comp.specification.z" at Oxford and messages posted
		  on either will automatically appear on both. A message
		  answering some frequently asked questions is maintained and
		  sent to the list once a month. A list of back issues of
		  newsletters and other Z-related material is available
		  electronically via anonymous FTP from
		  \verb"ftp.comlab.ox.ac.uk:/pub/Zforum" in the file
		  \verb"00index" or via e-mail from the OUCL archive server
		  \cite{z:zzarc}. For messages from a particular month (e.g.,
		  May 1995), access a file such as \verb"zforum95-05"; for
		  the most recent messages, see the file \verb"zforum".}
}