[Z in Practice] Rosalind Barden, Susan Stepney, and David Cooper.
Z in Practice .

BCS Practitioner Series. Prentice-Hall, 1994.

Bibliography

[Barden et al 1992]
Rosalind Barden, Susan Stepney, and David Cooper. The use of Z . In [Nicholls 1992] , pages 99--124.

[Barrett 1989]
Geoff Barrett. Formal methods applied to a floating-point number system. IEEE Transactions on Software Engineering , SE-15(5):611--621, May 1989.

[Bentley et al 1986]
Jon Bentley , Donald E. Knuth , and Doug McIlroy. Programming pearls: a literate program. Communications of the ACM , 29(6):471--483, 1986.

[Björner et al 1990]
Dines Björner, C. A. R. Hoare, and H. Langmaack, editors. VDM'90: VDM and Z---Formal Methods in Software Development, Kiel , volume 428 of Lecture Notes in Computer Science . Springer Verlag, 1990.

[Blyth 1990]
David Blyth. The CICS application programming interface: Temporary storage. IBM Technical Report TR12.301, IBM UK, Hursley Park, December 1990.

[Booch 1994]
Grady Booch . Object-Oriented Analysis and Design with Applications . Benjamin-Cummings, 2nd edition, 1994.

[Bowen & Hall 1994]
Jonathan P. Bowen and J. Anthony Hall, editors. Proceedings of the 8th Z User Meeting, Cambridge 1994 , Workshops in Computing. Springer Verlag, 1994.

[Bowen & Nicholls 1993]
Jonathan P. Bowen and John E. Nicholls, editors. Proceedings of the 7th Annual Z User Meeting, London 1992 , Workshops in Computing. Springer Verlag, 1993.

[Bowen 1987a]
Jonathan P. Bowen. Formal specification and documentation of microprocessor instruction sets. In H. Schumny and J. Mölgaard, editors, Proceedings of Euromicro '87, Microcomputers: Usage, Methods and Structures , volume 21(1--5) of Microprocessing and Microprogramming , pages 223--230. Elsevier North-Holland, August 1987.

[Bowen 1987b]
Jonathan P. Bowen. The formal specification of a microprocessor instruction set. Technical Monograph PRG-60, Programming Research Group, Oxford University Computing Laboratory, January 1987.

[Bowen 1989]
Jonathan P. Bowen. POS---formal specification of a UNIX tool. IEE Software Engineering Journal , 4(1):67--72, 1989.

[Brien & Nicholls 1992]
Stephen M. Brien and John E. Nicholls. Z base standard, version 1.0. ZIP document ZIP/PRG/92/121, SRC D-132, Oxford University PRG, November 1992.

[Brown et al 1986]
A. W. Brown, D. S. Robinson, and R. Weedon. Managing software development. In P. J. Brown and D. J. Barnes, editors, Software Engineering '86 , volume 6 of IEE Computing Series , pages 197--235. Peter Peregrinus, 1986.

[Bryant 1990]
A. Bryant. Structured methodologies and formal notations: Developing a framework for synthesis and investigation. In [Nicholls 1990] , pages 229--241.

[Carrington et al 1990]
David A. Carrington, David Duke, Roger Duke, Paul King, Gordon A. Rose, and Graeme Smith. Object-Z: An object-oriented extension to Z. In S. Vuong, editor, Formal Description Techniques II, FORTE'89 , pages 281--296. North-Holland, 1990.

[CESG 1991]
CESG. A formal development methodology for high confidence systems. CESG Computer Security Manual F, Communications-Electronics Security Group (L7), Government Communications Headquarters, Cheltenham, UK, February 1991.

[Chambers 1972]
Chambers Twentieth Century Dictionary . W & R Chambers, new edition, 1972.

[Clocksin & Mellish 1987]
W. F. Clocksin and C. S. Mellish. Programming in Prolog . Springer Verlag, 3rd edition, 1987.

[Cohen et al 1986]
Bernard Cohen, W. T. Harwood, and M. I. Jackson. The Specification of Complex Systems . Addison-Wesley, 1986.

[Cooper 1990]
David Cooper. Educating management in Z. In [Nicholls 1990] , pages 192--194.

[Delisle & Garlan 1990]
Norman Delisle and David Garlan. A formal specification of an oscilloscope. IEEE Software , pages 29--36, September 1990.

[Dick et al 1990]
A. J. J. Dick, P. J. Krause, and J. Cozens. Computer aided transformation of Z into Prolog. In [Nicholls 1990] , pages 71--85.

[Dijkstra 1979]
Edsgar W. Dijkstra. Structured programming. In Edward Yourdon, editor, Classics in Software Engineering . Yourdon Press, 1979.

[Diller 1990]
Antoni Diller. Z: An Introduction to Formal Methods . Wiley, 1990.

[Draper 1993]
Christine Draper. Practical experiences of Z and SSADM. In [Bowen & Nicholls 1993] .

[Duke & Duke 1990a]
David Duke and Roger Duke. Towards a semantics for Object-Z. In [Björner et al 1990] , pages 244--261.

[Duke & Duke 1990b]
Roger Duke and David Duke. Aspects of object-oriented formal specification. In Australian Software Engineering Conference , 1990.

[Duke et al 1990]
Roger Duke, Gordon A. Rose, and Anthony Lee. Object-oriented protocol specification. In L. Logrippoo, R. L. Probert, and H. Ural, editors, Protocol Specification, Testing and Verification 10 , pages 325--338. North-Holland, 1990.

[Duke et al 1991]
Roger Duke, Paul King, Gordon A. Rose, and Graeme Smith. The Object-Z specification language version 1. Technical Report 91-1, Software Verification Research Centre, Department of Computer Science, University of Queensland, May 1991.

[Fagan 1986]
M. E. Fagan. Advances in software inspections. IEEE Transactions on Software Engineering , SE-12(7):44--51, 1986.

[Gardner 1965]
Martin Gardner. Mathematical Puzzles and Diversions . Pelican, 1956.

[Garlan & Delisle 1990]
David Garlan and Norman Delisle. Formal specifications as reusable frameworks. In [Björner et al 1990] , pages 150--163.

[Gerhart 1990]
Susan L. Gerhart. Applications of formal methods: Developing virtuoso software. IEEE Software , pages 7--10, September 1990.

[Giovanni & Iachini 1990]
R. Di Giovanni and P. Luigi Iachini. HOOD and Z for the development of complex systems. In [Björner et al 1990] , pages 262--289.

[Goldberg & Robson 1983]
Adele Goldberg and David Robson. Smalltalk-80: The Language and its Implementation . Addison-Wesley, 1983.

[Goldberg 1984]
Adele Goldberg. Smalltalk-80: The Interactive Programming Environment . Addison-Wesley, 1984.

[Gravell 1991]
Andrew M. Gravell. What is a good formal specification? In [Nicholls 1991] , pages 137--150.

[Guindon 1990]
Raymonde Guindon. The knowledge exploited by experts during software system design. International Journal of Man--Machine Studies , 33(3):279--304, 1990.

[Hall 1990]
J. Anthony Hall. Using Z as a specification calculus for object-oriented systems. In [Björner et al 1990] , pages 290--318.

[Hall 1994]
J. Anthony Hall. Specifying and interpreting class hierarchies in Z. In [Bowen & Hall 1994] , pages 120--138.

[Halliwell 1985]
Leslie Halliwell. Halliwell's Film Guide . Granada Publishing, 5th edition, 1985.

[Hammond 1994]
Jonathan A. R. Hammond. Producing Z specifications from object-oriented analysis. In [Bowen & Hall 1994] , pages 316--336.

[Hayes & Jones 1991]
Ian J. Hayes and Cliff B. Jones. Specifications are not (necessarily) executable. IEE Software Engineering Journal , pages 330--338, November 1991.

[Hayes 1990]
Ian J. Hayes. A generalisation of bags in Z. In [Nicholls 1990] , pages 113--127.

[Hayes 1991]
Ian J. Hayes. Interpretations of Z schema operators. In [Nicholls 1991] , pages 12--26.

[Hayes 1993a]
Ian J. Hayes. Flexitime specification. In [Hayes 1993b] .

[Hayes 1993b]
Ian J. Hayes, editor. Specification Case Studies . Prentice Hall, 2nd edition, 1993.

[Hee et al 1991]
K. M. van Hee, L. J. Somers, and M. Voorhoeve. Z and high level Petri nets. In [Prehn & Toetenel 1991] , pages 204--219.

[Helm et al 1990]
Richard Helm, Ian M. Holland, and Dipayan Gangopadhyay. Contracts: Specifying behavioral compositions in object-oriented systems. OOPSLA/ECOOP'90 Proceedings, ACM SIGPLAN Notices , 25(10):169--180, 1990.

[Houston & King 1991]
Iain S. C. Houston and Steve King. CICS project report: Experience and results from the use of Z in IBM. In [Prehn & Toetenel 1991] , pages 588--596.

[Houston & Wordsworth 1990]
Iain S. C. Houston and John B. Wordsworth. A Z specification of part of the CICS file control API. IBM Technical Report TR12.272, IBM UK, Hursley Park, February 1990.

[Imperato 1991]
Michael Imperato. An Introduction to Z . Chartwell-Bratt, 1991.

[inmos]
inmos. IMS T800 architecture. Technical Note 6.

[Jacob 1991]
Jeremy Jacob. The varieties of refinement. In [Morris & Shaw 1991] , pages 441--455.

[Johnson & Sanders 1990]
M. Johnson and P. Sanders. From Z specifications to functional implementations. In [Nicholls 1990] , pages 86--112.

[Johnson 1992]
Ralph E. Johnson . Documenting frameworks using patterns. OOPSLA'92 Proceedings, ACM SIGPLAN Notices , 27(10):63--76, October 1992.

[Jones 1980]
Cliff B. Jones. Software Development: a rigorous approach . Prentice Hall, 1980.

[Kemp 1988a]
Duncan H. Kemp. Specification of Viper1 in Z. RSRE Memorandum 4195, Royal Signals and Radar Establishment, September 1988.

[Kemp 1988b]
Duncan H. Kemp. Specification of Viper2 in Z. RSRE Memorandum 4217, Royal Signals and Radar Establishment, October 1988.

[King & Sörensen 1989]
Steve King and Ib Holm Sörensen. Specification and design of a library system. In John A. McDermid, editor, The Theory and Practice of Refinement: Approaches to the Formal Development of Large-Scale Software Systems . Butterworths, 1989.

[King et al 1988]
Steve King, Ib Holm Sörenson, and James C. P. Woodcock. Z: Grammar and concrete and abstract syntaxes. Technical Monograph PRG-68, Programming Research Group, Oxford University Computing Laboratory, 1988.

[King 1990a]
Steve King. The CICS application programming interface: Program control. IBM Technical Report TR12.302, IBM UK, Hursley Park, December 1990.

[King 1990b]
Steve King. Z and the refinement calculus. In [Björner et al 1990] , pages 164--188.

[Lano & Haughton 1994]
Kevin Lano and Howard Haughton, editors. Object-Oriented Specification Case Studies . The Object-Oriented series. Prentice Hall, 1994.

[Lightfoot 1991]
David Lightfoot. Formal Specification Using Z . Computer Science series. Macmillan, 1991.

[Lucas 1884]
Édouard Lucas. La tour d'hanoï. Science et Nature , 1(8):127--128, 1884.

[Lupton 1991]
Peter J. Lupton. Promoting forward simulation. In [Nicholls 1991] , pages 27--49.

[Macdonald 1991]
Ruaridh Macdonald. Z usage and abusage. RSRE Memorandum 91003, Royal Signals and Radar Establishment, February 1991.

[MacLean et al 1994]
Roy MacLean, Susan Stepney, Simon Smith, Nick Tordoff, David Gradwell, Tim Hoverd, and Simon Katz. Analysing Systems: determining requirements for object oriented development . BCS Practitioners Series. Prentice Hall, 1994.

[Mahoney & Hayes 1991]
Brendan Mahoney and Ian J. Hayes. A case study in timed refinement: A central heater. In [Morris & Shaw 1991] , pages 138--149.

[Mander et al 1994]
Keith C. Mander, Fiona Polack, and Mark Whiston. Software quality assurance using the SAZ method. In [Bowen & Hall 1994] .

[May 1990]
David May. Use of formal methods by a silicon manufacturer. In C. A. R. Hoare, editor, Developments in Concurrency and Communication , University of Texas at Austin Year of Programming series, pages 107--129. Addison-Wesley, 1990.

[McMorran & Powell 1993]
Mike A. McMorran and Steve Powell. Z Guide for Beginners . Blackwell Scientific, 1993.

[Meyer 1988]
Bertrand Meyer. Object-oriented Software Construction . Prentice Hall, 1988.

[Mitchell et al 1991]
Richard Mitchell, Martin Loomes, and John Howse. Organising specifications: a case study. Technical Report BPC 91/1, Brighton Polytechnic, Department of Computing, January 1991.

[MoD 1991]
The procurement of safety critical software in defence equipment. Interim Defence Standard 00-55 / Issue 1, UK Ministry of Defence, April 1991.

[Morgan & Sanders 1989]
C. Carroll Morgan and Jeff W. Sanders. Laws of the logical calculi. Technical Monograph PRG-78, Programming Research Group, Oxford University Computing Laboratory, September 1989.

[Morgan & Sufrin 1993]
C. Carroll Morgan and Bernard A. Sufrin. Specification of the Unix filing system. In [Hayes 1993b] .

[Morgan 1990]
C. Carroll Morgan. Programming from Specifications . Prentice Hall, 1990.

[Morris & Shaw 1991]
Joseph M. Morris and Roger C. Shaw, editors. 4th Refinement Workshop . Workshops in Computing. Springer Verlag, 1991.

[Mundy & Wordsworth 1990]
P. Mundy and John B. Wordsworth. The CICS application programming interface: Transient data and storage control. IBM Technical Report TR12.299, IBM UK, Hursley Park, October 1990.

[Nash 1990]
Trevor C. Nash. Using Z to describe large systems. In [Nicholls 1990] , pages 150--178.

[Nicholls 1990]
John E. Nicholls, editor. Z User Workshop: Proceedings of the 4th Annual Z User Meeting, Oxford 1989 , Workshops in Computing. Springer Verlag, 1990.

[Nicholls 1991]
John E. Nicholls, editor. Proceedings of the 5th Annual Z User Meeting, Oxford 1990 , Workshops in Computing. Springer Verlag, 1991.

[Nicholls 1992]
John E. Nicholls, editor. Proceedings of the 6th Annual Z User Meeting, York 1991 , Workshops in Computing. Springer Verlag, 1992.

[Nix & Collins 1988]
Christopher J. Nix and B. Peter Collins. The use of software engineering, including the Z notation, in the development of CICS. Quality Assurance , 14(3):103--110, September 1988.

[Norman 1980]
Barry Norman. The Hollywood Greats . Arrow, 1980.

[Parker 1991]
Colin E. Parker. Z tools catalogue. ZIP document ZIP/BAe/90/020, British Aerospace, Warton, May 1991.

[Phillips 1960]
Hubert Phillips. The Pan Book of Card Games . Pan, 1960.

[Polack et al 1993]
Fiona Polack , Mark Whiston, and Keith C. Mander. The SAZ project: Integrating SSADM and Z. In James C. P. Woodcock and P. G. Larson, editors, FME'93: Industrial-Strength Formal Methods , volume 670 of Lecture Notes in Computer Science . Springer Verlag, 1993.

[Polack et al 1994]
Fiona Polack, Mark Whiston, and Keith C. Mander. The SAZ method version 1.1. Technical Report YCS 207, Department of Computer Science, University of York, 1994.

[Potter et al 1991]
Ben Potter, Jane Sinclair, and David Till . An Introduction to Formal Specification and Z . Prentice Hall, 1991.

[Prehn & Toetenel 1991]
S. Prehn and W. J. Toetenel, editors. VDM'91: Formal Software Development Methods, Noordwijkerhout, Volume 1: Conference Contributions , volume 551 of Lecture Notes in Computer Science . Springer Verlag, 1991.

[Rose 1992]
Gordon A. Rose. Object-Z. In [Stepney et al 1992] , chapter 6, pages 59--77.

[Semmens & Allen 1991]
Lesley Semmens and Pat Allen. Using Yourdon and Z: An approach to formal specification. In [Nicholls 1991] , pages 228--253.

[Shepherd & Wilson 1989]
David Shepherd and Greg Wilson. Making chips that work. New Scientist , 1664:61--64, May 1989.

[Shipman 1982]
David Shipman. The Story of the Cinema , volume 1. Hodder and Stoughton, 1982.

[Smith & Duke 1989]
Graeme Smith and Roger Duke. Specification and verification of a cache coherence protocol. Technical Report 126, Department of Computer Science, University of Queensland, August 1989.

[Spivey 1988]
J. Michael Spivey. Understanding Z: a specification language and its formal semantics , volume 3 of Cambridge Tracts in Theoretical Computer Science . Cambridge University Press, 1988.

[Spivey 1992]
J. Michael Spivey. The Z Notation: a Reference Manual . Prentice Hall, 2nd edition, 1992.

[SSADM 1986]
Manchester NCC. SSADM Manual Version 3 , 1986.

[SSADM 1990]
Manchester NCC. SSADM Manual Version 4 , 1990.

[Steggles & Hulance 1994]
Pete Steggles and Jason Hulance. Z tools survey. Technical report, Imperial Software Technology, Cambridge, UK, June 1994.

[Stepney & Lord 1987]
Susan Stepney and Stephen P. Lord. Formal specification of an access control system . Software---Practice and Experience , 17(9):575--593, 1987.

[Stepney et al 1992]
Susan Stepney, Rosalind Barden, and David Cooper, editors. Object Orientation in Z . Workshops in Computing. Springer Verlag, 1992.

[Sterling & Shapiro 1986]
Leon Sterling and Ehud Shapiro. The Art of Prolog: Advanced Programming Techniques . MIT Press, 1986.

[Stewart & Tall 1977]
Ian Stewart and David Tall. The Foundations of Mathematics . Oxford University Press, 1977.

[Stewart 1992]
Ian Stewart. Another Fine Math You've Got Me Into . W. H. Freeman, 1992.

[Turner 1986]
David Turner. An overview of Miranda. ACM SIGPLAN Notices , 21(12):158--166, 1986.

[Valentine 1993]
Sam Valentine. Putting numbers into the mathematical toolkit. In [Bowen & Nicholls 1993] .

[Wegner 1987a]
Peter Wegner . Dimensions of object-based language design. OOPSLA'87 Proceedings, ACM SIGPLAN Notices , 22(12):168--182, 1987.

[Wegner 1987b]
Peter Wegner. The object-oriented classification paradigm. In Bruce Shriver and Peter Wegner, editors, Research Directions in Object-Oriented Programming . MIT Press, 1987.

[Wells 1987]
David Wells. The Penguin Dictionary of Curious and Interesting Numbers . Penguin, revised edition, 1987.

[West & Eaglestone 1989]
Margaret M. West and Barry M. Eaglestone. Software development: Two approaches to animation of Z specifications using Prolog. IEE Software Engineering Journal , pages 264--276, July 1989.

[West et al 1992]
Margaret M. West, T. F. Buckley, and P. H. Jesty. Pelican safety study. Research Report 92.4, University of Leeds, School of Computer Studies, March 1992.

[Wikström 1987]
Å. Wikström. Functional Programming using Standard ML . Prentice Hall, 1987.

[Woodcock & Brien 1992]
James C. P. Woodcock and Stephen M. Brien. W : A logic for Z. In [Nicholls 1992] , pages 77--96.

[Woodcock & Davies 1996]
Jim Woodcock and Jim Davies. Using Z: Specification, Refinement, and Proof . Prentice Hall, 1996.

[Woodcock & Loomes 1988]
James C. P. Woodcock and Martin Loomes. Software Engineering Mathematics . Pitman, 1988.

[Woodcock 1989]
James C. P. Woodcock. Structuring specifications in Z. IEE Software Engineering Journal , 4(1):51--66, 1989.

[Woodcock 1991]
James C. P. Woodcock. An introduction to refinement in Z. ZIP document ZIP/RAL/92/005, Rutherford Appleton Laboratories, October 1991.

[Worden 1991]
Robert Worden. The process of refinement. In [Morris & Shaw 1991] , pages 1--5.

[Wordsworth 1989a]
John B. Wordsworth. Practical experience of formal specification: a programming interface for communications. In Proceedings of ESEC'89 , number 387 in Lecture Notes in Computer Science. Springer Verlag, 1989.

[Wordsworth 1989b]
John B. Wordsworth. A Z development method. Draft version 0.11, IBM UK, Hursley Park, January 1989.

[Wordsworth 1992]
John B. Wordsworth. Software Development with Z . Addison-Wesley, 1992.