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.