Skip to main content
SpringerLink
Log in

Selected Z Bibliography

  • Conference paper
Z User Workshop, Oxford 1990

Part of the book series: Workshops in Computing ((WORKSHOPS COMP.))

  • 55 Accesses

Abstract

This bibliography contains a list of Z references that are either available from the librarian or via electronic mail at the Programming Research Group (PRG), or as published papers, books or technical reports from other institutions. The bibliography is in alphabetical order by author name(s).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Gregory D. Abowd. Agents: Communicating interactive processes. In Dan Diaper, David Gilmore, Gilbert Cockton, and Brian Shackel, editors, Human-Computer Interaction — INTERACT 90, pages 143–148. Elsevier Science Publishers, 1990.

    Google Scholar 

  2. Gregory D. Abowd, Jonathan P. Bowen, Alan Dix, Michael Harrison, and Roger Took. User interface languages: a survey of existing methods. Technical Report PRG-TR-5–89, Oxford University Computing Laboratory, 11 Keble Road, Oxford, UK, October 1989.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.

    Google Scholar 

  3. Jean-Raymond Abrial. The B tool. In G. Goos and J. Hartmanis, editors, VDM — The Way Ahead. Proc. 2nd VDM-Europe Symposium, volume 328 of Lecture Notes in Computer Science, pages 86–87. VDM-Europe, Springer-Verlag, 1988.

    Google Scholar 

  4. Jean-Raymond Abrial, S.A. Schuman, and B. Meyer. Specification language. In R.M. McKeag and A.M. Macnaghten, editors, On the Construction of Programs: An Advanced Course, pages 343–410. Cambridge University Press, UK, 1980.

    Google Scholar 

  5. Jean-Raymond Abrial and Ib H. Sorensen. KWIC-index generation. In J. Staunstrup, editor, Program Specification: Proceedings of a Workshop, volume 134 of Lecture Notes in Computer Science, pages 88–95. Springer-Verlag, 1981

    Google Scholar 

  6. D.B. Arnold, D.A. Duce, and G.J. Reynolds. An approach to the formal specification of configurable models of graphs systems. In Guy Maréchal, editor, Proc. European Computer Graphics Conference and Exhibition, pages 439–463. EUROGRAPHICS87, Elsevier Science Publishers B. V. ( North-Holland ), 1987. The paper describes a general framework for the formal specification of modular graphics systems. The approach is illustrated by an example taken from the Graphical Kernel System (GKS) and uses the Z specification notation.

    Google Scholar 

  7. M. Bailey. Formal specification using Z. In Proc. Software Engineering anniversary meeting (SEAS), page 99. SEA, 1987.

    Google Scholar 

  8. Geoff Barrett. Formal methods applied to a floating-point number system. IEEE Transactions on Software Engineering, 15(5):611–621, May 1989.This paper presents a formalisation of the IEEE standard for binary floating-point arithmetic in Z. The formal specification is refined into four components. The procedures presented form the basis for the floating-point unit of the Inmos IMS T800 tra nsputer. This work resulted in a joint Queens Award for technological achievement for Inmos Ltd. and the Oxford University Computing Laboratory in 1990. It is estimated that the approach used saved a year in development time compared to traditional methods.

    Google Scholar 

  9. Geoff Barrett. Formal methods applied to a floating-point number system. IEEE Transactions on Software Engineering, 15(5):611–621, May 1989.This paper presents a formalisation of the IEEE standard for binary floating-point arithmetic in Z. The formal specification is refined into four components. The procedures presented form the basis for the floating-point unit of the Inmos IMS T800 tra nsputer. This work resulted in a joint Queens Award for technological achievement for Inmos Ltd. and the Oxford University Computing Laboratory in 1990. It is estimated that the approach used saved a year in development time compared to traditional methods.

    Google Scholar 

  10. S. Baxter. Executing Z specifications. Research and Technology memorandum RT31/009/88, British Telecom Research Laboratories, Martlesham Heath, Ipswich, Suffolk, UK, 1988.

    Google Scholar 

  11. Mike Benjamin. A message passing system: An example of combining CSP and Z. In John E. Nicholls, editor, Z User Workshop, Oxford 1989, Workshops in Computing, pages 221–228. Springer-Verlag, 1990.

    Google Scholar 

  12. Marc Benveniste. Operational semantics of a distributed object-oriented language and its Z formal specification. IRISA Technical Report 532, IRISA, Campus de Beaulieu, F-35042, Rennes Cedex, France, April 1990. This report presents a Z specification of the operational semantics of a parallel object-based language, super-set of Modula-2. The specification is type-checked with J.M. Spiveys fuzz [156]. The report will be also available as an INRIA publication.

    Google Scholar 

  13. S. Bera. Structuring for the VDM specification language. In G. Goos and J. Hartmanis, editors, VDM–The Way Ahead. Proc. 2nd VDM-Europe Symposium, volume 328 of Lecture Notes in Computer Science, pages 2–25. VDM-Europe, Springer-Verlag, 1988.

    Google Scholar 

  14. M.A. Best. Specification of a Z cross-reference facility. IBM Technical Report TR12.253, IBM United Kingdom Laboratories Ltd., Hursley Park, Winchester, Hampshire 5021 2JN, UK, September 1986.

    Google Scholar 

  15. D. Bjprner, C.A.R. Hoare, and H. Langmaack, editors. VDM and Z - Formal Methods in Software Development, volume 428 of Lecture Notes in Computer Science. VDM-Europe, Springer-Verlag, 1990. Proc. Third International Symposium of VDM-Europe, 17–21 April 1990, Kiel, Germany. A number of papers concerned with Z were presented [38, 50, 60, 66, 67, 71, 100, 142, 162, 176, 194].

    Google Scholar 

  16. David Blyth. The CICS application programming interface: Temporary storage. IBM Technical Report TR12.301, IBM United Kingdom Laboratories Ltd., Hursley Park, Winchester, Hampshire 5021 2JN, UK, December 1990. One of a number of reports on the CICS application programming interface. See also [86, 99, 124].

    Google Scholar 

  17. Jonathan P. Bowen. Formal specification and documentation of microprocessor instruction sets. In Harald Schumny and John Molgaard, editors, Proc. Euromicro 87, Microcomputers: Usage, Methods and Structures, volume 21, pages 223–230. EUROMICRO, Elsevier Science Publishers B.V. ( North-Holland ), August 1987.

    Google Scholar 

  18. Jonathan P. Bowen. The formal specification of a microprocessor instruction set. Technical Monograph PRG-60, Oxford University Computing Laboratory, 11 Keble Road, Oxford, UK, January 1987. The Z notation is used to define the Motorola M6800 8-bit microprocessor instruction set.

    Google Scholar 

  19. Jonathan P. Bowen, editor. Proc. Z Users Meeting, I Wellington Square, Oxford, 11 Keble Road, Oxford, UK, December 1987. Oxford University Computing Laboratory. The 1987 Z Users Meeting was held on Friday 8 December at the Department of External Studies, Rewley House, 1 Wellington Square, Oxford, UK. The LATEX [104] source of the Proceedings is available by sending the command

    Google Scholar 

  20. Jonathan P. Bowen. Formal specification in Z as a design and documentation tool. In Proc. Second IEE/BCS Conference on Software Engineering, volume 290, pages 164–168. IEE/BCS, July 1988.

    Google Scholar 

  21. Jonathan P. Bowen, editor. Proc. Third Annual Z Users Meeting, 11 Keble Road, Oxford, UK, December 1988. Oxford University Computing Laboratory. The 1988 Z Users Meeting was held on Friday 16 December at the Department of External Studies, Rewley House, 1 Wellington Square, Oxford, UK. Issued with A Miscellany of Handy Techniques by Ruaridh Macdonald, RSRE (9 pages), Practical Experience of Formal Specification: a programming interface for communications by John B. Wordsworth, IBM (18 pages), and a number of posters (20 pages). This is available from the Librarian at the PRG. The LATEX [104] source file for the main part of the document is available by sending the command send z proc88.tex via

    Google Scholar 

  22. Jonathan P. Bowen. Formal specification of window systems. Technical Monograph PRG-74, Oxford University Computing Laboratory, 11 Keble Road, Oxford, UK, June 1989. Three existing window systems, X from MIT, WM from Carnegie-Mellon University and the Blit from ATandT Bell Laboratories are covered.

    Google Scholar 

  23. Jonathan P. Bowen. POS: Formal specification of a UNIX tool. Software Engineering Journal, 4 (1): 67–72, January 1989.

    Article  Google Scholar 

  24. Jonathan P. Bowen. Formal specification of the ProCoS/safemos instruction set. Microprocessors and Microsystems, 14(10):631–643, December 1990. This article gives a preview of the work of two European government-sponsored projects investigating design methods for provable computer systems. a common interface both projects use subsets of Occam and the transputer instruction set. A number of transputer instructions are presented using Z. The article is part of a special issue on Formal aspects of microprocessor design, edited by Hussein Zedan. See also [148].

    Google Scholar 

  25. Jonathan P. Bowen. Z bibliography. Oxford University Computing Laboratory, February 1991. A master bibliography, maintained in BIBTEX database format, of both published and unpublished work related to Z. This is available via e-mail, together with a LATEX [104] file for printing the bibliography, by sending a message containing the command send z zbib.bib zbib. tex to the PRG archive server on 200]. Ruaridh Macdonald, RSRE, Malvern, initiated the Z bibliography and helped maintain it for a while. Joan Arnold, the industrial liaison secretary at the PRG, Oxford, will be helping to maintain it in the future. To add entries, please send as complete information as possible

    Google Scholar 

  26. Jonathan P. Bowen, Roger B. Gimson, and Stig Topp-Jorgensen. The specification of network services. Technical Monograph PRG-61, Oxford University Computing Laboratory, 11 Keble Road, Oxford, UK, August 1987.

    Google Scholar 

  27. Jonathan P. Bowen, Roger B. Gimson, and Stig Topp-Jorgensen. Specifying system implementations in Z. Technical Monograph PRG-63, Oxford University Computing Laboratory, 11 Keble Road, Oxford, UK, February 1988.

    Google Scholar 

  28. David J. Brown and Jonathan P. Bowen. The Event Queue: An extensible input system for UNIX workstations. In Proc. European Unix Users Group Conference, pages 29–52. EUUG, May 1987.

    Google Scholar 

  29. D. Brownbridge. Using Z to develop a CASE toolset. In John E. Nicholls, editor, Z User Workshop, Oxford 1989, Workshops in Computing, pages 142–149. Springer-Verlag, 1990.

    Google Scholar 

  30. T. Bryant. Structured methodologies and formal notations: Developing a framework for synthesis and investigation. In John E. Nicholls, editor, Z User Workshop, Oxford 1989, Workshops in Computing, pages 229–241. Springer-Verlag, 1990.

    Google Scholar 

  31. Alan Burns and I.W. Morrison. A formal description of the structure attribute model. Software Engineering Journal, 4 (2): 74–78, March 1989.

    Article  Google Scholar 

  32. Alan Burns and A.J. Wellings. Occams priority model and deadline scheduling. In Proc. 7th Occam User Group Meeting, Grenoble, 1987.

    Google Scholar 

  33. Alan Burns and A.J. Wellings. A formal description of Ada tasking in Z. Computer Science Report YCS122, University of York, Heslington, York YO1 5DD, UK, 1989.

    Google Scholar 

  34. Alan Burns and A.J. Wellings. Priority inheritance and message passing communication: A formal treatment. Computer Science Report YCS116, University of York, Heslington, York YO1 5DD, UK, 1989.

    Google Scholar 

  35. Paul Butcher. A behavioural semantics for Linda-2. Department of Computer Science, University of York, 1990.

    Google Scholar 

  36. D. Carrington, D. 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 (FORTE89), pages 281–296. North-Holland, 1990.

    Google Scholar 

  37. D. Carrington and Graeme Smith. Extending Z for object-oriented specifications. In Proc. 5th Australian Software Engineering Conference (ASWEC90), pages 9–14, 1990.

    Google Scholar 

  38. Patrice Chalin and Peter Grogono. Z specification of an object manager. In D. Bjorner, C.A.R. Hoare, and H. Langmaack, editors, VDM and Z — Formal Methods in Software Development, volume 428 of Lecture Notes in Computer Science, pages 41–71. VDM-Europe, Springer-Verlag, 1990.

    Chapter  Google Scholar 

  39. Bernie Cohen. Justification of formal methods for system specifications and A rejustification of formal notations. Software Engineering Journal, 4 (1): 26–38, January 1989.

    Article  Google Scholar 

  40. B.P. Collins, John E. Nicholls, and Ib H. Sorensen. Introducing formal methods: the CICS experience with Z. In B. Neumann et al., editors, Mathematical Structures for Software Engineering. Oxford University Press, UK, 1991.

    Google Scholar 

  41. David Cooper. Educating management in Z. In John E. Nicholls, editor, Z User Workshop, Oxford 1989, Workshops in Computing, pages 192–194. Springer-Verlag, 1990.

    Google Scholar 

  42. S. Croxall, Peter Lupton, and John B. Wordsworth. A formal specification of the CPI communications. IBM Technical Report TR12.277, IBM United Kingdom Laboratories Ltd., Hursley Park, Winchester, Hampshire 5021 2JN, UK, 1990.

    Google Scholar 

  43. Norman Delisle and David Garlan. Formally specifying electronic instruments. In Proc. Fifth International Workshop on Software Specification and Design. IEEE Computer Society, May 1989. Also published in ACM SIGSOFT Software Engineering Notes 14(3).

    Google Scholar 

  44. Norman Delisle and David Garlan. A formal specification of an oscilloscope. IEEE Software, pages 29–36, September 1990. Unlike most work on the application of formal methods, this research uses formal methods to gain insight into system architecture. The context for this case study is electronic instrument design.

    Google Scholar 

  45. A.J.J. Dick, P.J. Krause, and J. Cozens. Computer aided transformation of Z into Prolog. In John E. Nicholls, editor, Z User Workshop, Oxford 1989, Workshops in Computing, pages 71–85. Springer-Verlag, 1990.

    Google Scholar 

  46. Antoni Diller. Specifying interactive programs in Z. School of Computer Science Research Report CSRP-90–13, University of Birmingham, UK, August 1990.

    Google Scholar 

  47. Antoni Diller. Z: An Introduction to Formal Methods. Wiley, Chichester, UK, June 1990. his book offers a comprehensive tutorial to Z from the practical viewpoint. Many natural deduction style proofs are presented and exercises are included.

    Google Scholar 

  48. David A. Duce. A simple example from GKS in Z. Technical Report RAL-86–082, Informatics Division, Rutherford Appleton Laboratories, Chilton, Didcot, Oxon 0X11 OQX, UK, 1986.

    Google Scholar 

  49. D. Duke and Roger Duke. A history model for classes in Object-Z. Technical Report 120, Department of Computer Science, University of Queensland, Australia, 1989.

    Google Scholar 

  50. D. Duke and Roger Duke. Towards a semantics for Object-Z. In D. Bj0rner, C.A.R. Hoare, and H. Langmaack, editors, VDM and Z — Formal Methods in Software Development, volume 428 of Lecture Notes in Computer Science, pages 244–261. VDM-Europe, Springer-Verlag, 1990.

    Google Scholar 

  51. Roger Duke and D. Duke. Aspects of object-oriented formal specification. In Proc. 5th Australian Software Engineering Conference (ASWEC90), pages 21–26, 1990.

    Google Scholar 

  52. Roger Duke, Ian J. Hayes, Paul King, and Gordon A. Rose. Protocol specification and verification using Z. In S. Aggarwal and K. Sabnani, editors, Protocol Specification, Testing, and Verification VIII, pages 33–46. North-Holland, 1988.

    Google Scholar 

  53. Roger Duke and Gordon A. Rose. A complete Z specification of an interactive program editor. Technical Report 71, Department of Computer Science, University of Queensland, Australia, 4072, 1986.

    Google Scholar 

  54. Roger Duke, Gordon A. Rose, and A. Lee. Object-oriented protocol specification. In L. Logrippo, R.L. Probert, and H. Ural, editors, Protocol Specification, Testing, and Verification X, pages 325–338. North-Holland, 1990.

    Google Scholar 

  55. Roger Duke and Graeme Smith. Temporal logic and Z specifications. Australian Computer Journal, 21 (2): 62–66, May 1989.

    Google Scholar 

  56. E. Fergus and D. Ince. Z specifications and modal logic. In Patrick A.V. Hall, editor, Proc. Software Engineering 90, volume 1 of British Computer Society Conference Series. Cambridge University Press, July 1990.

    Google Scholar 

  57. L. William Flinn and Ib H. Sorensen. CAVIAR: A case study in specification. Technical Monograph PRG-48, Oxford University Computing Laboratory, 11 Keble Road, Oxford, UK, July 1985.

    Google Scholar 

  58. Mike Flynn, Tim Hoverd, and David Brazier. Formaliser — an interactive support tool for Z. In John E. Nicholls, editor, Z User Workshop, Oxford 1989, Workshops in Computing, pages 128–141. Springer-Verlag, 1990.

    Google Scholar 

  59. David Garlan. The role of reusable frameworks. ACM SIGSOFT Software Engineering Notes, 15 (4): 42–44, September 1990.

    Article  Google Scholar 

  60. David Garlan and Norman Delisle. Formal specifications as reusable frameworks. In D. Bjorner, C.A.R. Hoare, and H. Langmaack, editors, VDM and Z — Formal Methods in Software Development, volume 428 of Lecture Notes in Computer Science, pages 150–163. VDM-Europe, Springer-Verlag, 1990.

    Chapter  Google Scholar 

  61. Susan L. Gerhart. Applications of formal methods: Developing virtuoso software. IEEE Software, pages 6–10, September 1990.

    Google Scholar 

  62. Stephen Gilmore. Correctness-Oriented Approaches to Software Development. PhD thesis, Department of Computer Science, The Queens University of Belfast, Northern Ireland, UK, September 1990. Development of a specification source-to-source translator from Z to VDM/SL with Z, VDM and algebraic specifications and proofs of properties of the implementation.

    Google Scholar 

  63. Roger B. Gimson. The formal documentation of a Block Storage Service. Technical Monograph PRG-62, Oxford University Computing Laboratory, 11 Kehle Road, Oxford, UK, August 1987.

    Google Scholar 

  64. Roger B. Gimson and C. Carroll Morgan. Ease of use through proper specification. In David A. Duce, editor, Distributed Computing Systems Programme. Peter Peregrinus, London, UK, 1984.

    Google Scholar 

  65. Roger B. Gimson and C. Carroll Morgan. The Distributed Computing Software project. Technical Monograph PRG-50, Oxford University Computing Laboratory, 11 Keble Road, Oxford, UK, July 1985.

    Google Scholar 

  66. R. Di Giovanni and P.L. Iachini. HOOD and Z for the development of complex systems. In D. Bjorner, C.A.R. Hoare, and H. Langmaack, editors, VDM and Z — Formal Methods in Software Development, volume 428 of Lecture Notes in Computer Science, pages 262–289. VDM-Europe, Springer-Verlag, 1990.

    Chapter  Google Scholar 

  67. Reinhard Gotzhein. Specifying open distributed systems with Z. In D. Bjorner, C.A.R. Hoare, and H. Langmaack, editors, VDM and Z — Formal Methods in Software Development, volume 428 of Lecture Notes in Computer Science, pages 319–339. VDM-Europe, Springer-Verlag, 1990.

    Chapter  Google Scholar 

  68. Andy M. Gravell. Minimisation in formal specification and design. In John E. Nicholls, editor, Z User Workshop, Oxford 1989, Workshops in Computing, pages 32–45. Springer-Verlag, 1990.

    Google Scholar 

  69. Frank Halasz and Mayer Schwartz. The Dexter hypertext reference model. In NIST Hypertext Standardization Workshop, January 1990.

    Google Scholar 

  70. Anthony Hall. Seven myths of formal methods. IEEE Software, pages 11–19, September 1990. Formal methods are difficult, expensive, and not widely useful, detractors say. Using a case study and other real-world examples, this article challenges such common myths.

    Google Scholar 

  71. J.A. Hall. Using Z as a specification calculus for object-oriented systems. In D. Bjorner, C.A.R. Hoare, and H. Langmaack, editors, VDM and Z — Formal Methods in Software Development, volume 428 of Lecture Notes in Computer Science, pages 290–318. VDM-Europe, Springer-Verlag, 1990.

    Chapter  Google Scholar 

  72. Patrick A.V. Hall. Towards testing with respect to formal specification. In Proc. Second IEE/BCS Conference on Software Engineering, volume 290, pages 159–163, Liverpool, UK, July 1988, July 1988. IEE/BCS.

    Google Scholar 

  73. Clare L. Harrold. Formal specification of a secure document control system for SMITE. RSRE Report no. 88002, Royal Signals and Radar Establishment, Ministry of Defence, Malvern, UK, February 1988.

    Google Scholar 

  74. Howard Haughton and Kevin C. Lano. Three dimensional maintenance. In Malcolm Munro and Peter Carroll, editors, Fourth Software Maintenance Workshop Notes, 18–20 September 1990. Centre for Software Maintenance, Durham, UK, 1990. This paper presents an object-oriented extension to Z with the aim to aid software maintenance.

    Google Scholar 

  75. Ian J. Hayes. Applying formal specification to software development in industry. IEEE Transactions on Software Engineering, 11 (2): 169–178, February 1985.

    Google Scholar 

  76. Ian J. Hayes. Specification case studies. Technical Monograph PRG-46, Oxford University Computing Laboratory, 11 Keble Road, Oxford, UK, July 1985 uperseded by [80].

    Google Scholar 

  77. Ian J. Hayes. Specification directed module testing. Technical Monograph PRG-49, Oxford University Computing Laboratory, 11 Keble Road, Oxford, UK, July 1985.

    Google Scholar 

  78. Ian J. Hayes. Specifying the CICS application programmers interface. Technical Monograph PRG-47, Oxford University Computing Laboratory, 11 Keble Road, Oxford, UK, July 1985.

    Google Scholar 

  79. Ian J. Hayes. Using mathematics to specify software. In Proc. First Australian Software Engineering Conference. Institution of Engineers, Australia, May 1986.

    Google Scholar 

  80. Ian J. Hayes, editor. Specification Case Studies. International Series in Computer Science. Prentice Hall, Hemel Hempstead, Hertfordshire HP2 4RG, UK, 1987. This book contains material from PRG Technical Monographs 46–50 [76, 78, 57, 77, 65]. It is edited by Ian Hayes and written mainly by members of the PRG. The contributors are Ian J. Hayes, L. William Flinn, Roger B. Gimson, C. Carroll Morgan, Ib H. Sorensen and Bernard A. Sufrin. The book forms a varied collection of case studies using Z.

    Google Scholar 

  81. Ian J. Hayes. A generalisation of bags in Z. In John E. Nicholls, editor, Z User Workshop, Oxford 1989, Workshops in Computing, pages 113–127. Springer-Verlag, 1990.

    Google Scholar 

  82. Ian J. Hayes. Specification of an oscilloscope. Department of Computer Science, University of Queensland, 1990.

    Google Scholar 

  83. He Jifeng, C.A.R. Hoare, and J.W. Sanders. Data refinement refined. In B. Robinet and R. Wilhelm, editors, Proc. ESOP 86, volume 213 of Lecture Notes in Computer Science, pages 187–196. Springer-Verlag, 1986.

    Google Scholar 

  84. Brian Hepworth. ZIP: a unification initiative for Z standards, methods and tools. In John E. Nicholls, editor, Z User Workshop, Oxford 1989, Workshops in Computing, pages 253–259. Springer-Verlag, 1990.

    Google Scholar 

  85. Brian Hepworth. ZIP project overview. DTI IED Project No. 1639 Report ZIP/BAe/90/017, Software Technology Department, British Aerospace, Warton PR4 1AX, UK, December 1990.

    Google Scholar 

  86. Ian S.C. Houston. The CICS application programming interface: Automatic transaction initiation. IBM Technical Report TR12.300, IBM United Kingdom Laboratories Ltd., Hursley Park, Winchester, Hampshire 5021 2JN, UK, December 1990.One of a number of reports on the CICS application programming interface. See also [16, 99, 124].

    Google Scholar 

  87. Ian S.C. Houston and John B. Wordsworth. A Z specification of part of the CICS file control API. IBM Technical Report TR12.272, IBM United Kingdom Laboratories Ltd., Hursley Park, Winchester, Hampshire 5021 2JN, UK, 1990.

    Google Scholar 

  88. IEEE Software. IEEE Computer Society, September 1990. Special issue on Formal Methods.This is a special issue on Formal Methods with an emphasis on Z in particular. Published in conjunction with special Formal Methods issues of IEEE Transactions on Software Engineering and IEEE Computer. See also [44, 61, 70, 125, 161, 180].

    Google Scholar 

  89. Darrell C. Ince. An Introduction to Discrete Mathematics and Formal System Specification. Oxford Applied Mathematics and Computing Science Series. Oxford University Press, UK, 1988.

    Google Scholar 

  90. Inmos Ltd. Specification of instruction set and Specification of floating point unit instructions. In Transputer Instruction Set — A compiler writers guide, pages 127–161. Prentice Hall, Hemel Hempstead, Hertfordshire HP2 4RG, UK, 1988.Appendices F and G use a Z-like notation to give a specification of the instruction set of the IMS T212 and T414 transputers, and the T800 floating-point tra nsputer.

    Google Scholar 

  91. Jonathan Jacky. Formal specifications for a clinical cyclotron control system. ACM SIGSOFT Software Engineering Notes, 15 (4): 45–54, September 1990.

    Article  Google Scholar 

  92. M. Johnson and P. Sanders. From Z specifications to functional implementations. In John E. Nicholls, editor, Z User Workshop, Oxford 1989, Workshops in Computing, pages 86–112. Springer-Verlag, 1990.

    Google Scholar 

  93. P. Johnson. Using Z to specify CICS. In Proc. Software Engineering anniversary meeting (SEAS), page 303. SEA, 1987.

    Google Scholar 

  94. Mark Josephs. The data refinement calculator for Z specifications. Information Processing Letters, 27 (1): 29–33, 1988.

    Article  MathSciNet  Google Scholar 

  95. Mark Josephs. A state-based approach to communicating processes. Distributed Computing, 3:9–18, 1988.A theoretical paper on combining features of CSP and Z.

    Google Scholar 

  96. D.H. Kemp. Specification of Viperl in Z. RSRE Memorandum no. 4195, Royal Signals and Radar Establishment, Ministry of Defence, Malvern, UK, October 1988.

    Google Scholar 

  97. D.H. Kemp. Specification of Viper2 in Z. RSRE Memorandum no. 4217, Royal Signals and Radar Establishment, Ministry of Defence, Malvern, UK, October 1988.

    Google Scholar 

  98. Paul King. Printing Z and Object-Z ISTEX documents. Department of Computer Science, University of Queensland, May 1990. A description of a Z style option oz.sty, an extended version of Mike Spiveys zed. sty [160], for use with the LATEX document preparation system [104]. It is particularly useful for printing Object-Z documents [36, 50]. The style file and the guide are available electronically by sending

    Google Scholar 

  99. Steve King. The CICS application programming interface: Program control. IBM Technical Report TR12.302, IBM United Kingdom Laboratories Ltd., Hursley Park, Winchester, Hampshire 5021 2JN, UK, December 1990.One of a number of reports on the CICS application programming interface. See also [16, 86, 124].

    Google Scholar 

  100. Steve King. Z and the refinement calculus. In D. Bjorner, C.A.R. Hoare, and H. Langmaack, editors, VDM and Z–Formal Methods in Software Development, volume 428 of Lecture Notes in Computer Science, pages 164–188. VDM-Europe, Springer-Verlag, 1990.

    Chapter  Google Scholar 

  101. Steve King. Z and the refinement calculus. Technical Monograph PRG-79, Oxford University Computing Laboratory, 11 Keble Road, Oxford, UK, February 1990. lso published as [100].

    Google Scholar 

  102. Steve King and Ib H. Sorensen. Specification and design of a library system. In The Theory and Practice of Refinement: Approaches to the Formal Development of Large-Scale Software Systems. Butterworths, London, UK, 1989.

    Google Scholar 

  103. Steve King, Ib H. Sorensen, and James C.P. Woodcock. Z: Grammar and concrete and abstract syntaxes. Technical Monograph PRG-68, Oxford University Computing Laboratory, 11 Keble Road, Oxford, UK, 1988.

    Google Scholar 

  104. Leslie Lamport. LATEX Users Guide 8 Reference Manual. Addison-Wesley Publishing Company, Reading, Massachusetts, USA, 1986. Z specifications may be produced using the document preparation system LATEX together with a special LATEX style option. The most widely used style files are fuzz. sty [156], zed. sty [160] and oz. sty [98].

    Google Scholar 

  105. Kevin Lano and Peter T. Breuer. From programs to Z specifications. In John E. Nicholls, editor, Z User Workshop, Oxford 1989, Workshops in Computing, pages 46–70. Springer-Verlag, 1990.

    Google Scholar 

  106. Ralph L. London. Specifying reusable components using Z: Sets implemented by bit vectors. Technical Report CR-88–14, Tektronix Laboratories, P.O. Box 500, MS 50–662, Beaverton, Oregon 97077, USA, November 1988.

    Google Scholar 

  107. is also in the Proceedings of the Fifth International Workshop on Software Specification and Design, Pittsburgh, Pennsylvania, 19–20 May 1989.

    Google Scholar 

  108. Ralph L. London and Kathleen R. Milsted. Specifying reusable components using Z: Realistic sets and dictionaries. ACM SIGSOFT Software Engineering Notes, 14 (3): 120–127, May 1989.

    Google Scholar 

  109. John A. McDermid. Special section on Z. Software Engineering Journal, 4(1):25–72, January 1989.A special issue on Z, introduced and edited by Prof. John McDermid. See also [23, 158, 189].

    Google Scholar 

  110. John A. McDermid, editor. The Theory and Practice of Refinement: Approaches to the Formal Development of Large-Scale Software Systems. Butterworths, London, UK, 1989.Papers from the Refinement Workshop at the University of York, held on 7–8 January 1988, including several on Z.

    Google Scholar 

  111. John A. McDermid. Formal methods: Use and relevance for the development of safety critical systems. In P.A. Bennett, editor, Safety Aspects of Computer Control. Butterworth Heineman, 1991. To appear.This paper discusses a number of formal methods and summarises strengths and weaknesses in safety critical applications; a major safety-related example is presented in Z.

    Google Scholar 

  112. Mike A. McMorran and John E. Nicholls. Z user manual. Technical Report TR12.274, IBM United Kingdom Laboratories Ltd., Hursley Park, Winchester, Hampshire SO21 2JN, UK, July 1989. Version 1. 0.

    Google Scholar 

  113. B. Meyer. On formalism in specifications. IEEE Software, 2 (1): 6–26, January 1985.

    Article  Google Scholar 

  114. Brian Q. Monahan. Book review. Formal Aspects of Computing, 1(1):137–142, January—March 1989. review of Understanding Z: A Specification Language and Its Formal Semantics by J.M. Spivey [159].

    Google Scholar 

  115. C. Carroll Morgan. Data refinement using miracles. Information Processing Letters, 26(5):243–246, January 1988. lso reprinted in [121].

    Google Scholar 

  116. C. Carroll Morgan. Procedures, parameters, and abstraction: Separate concerns. Science of Computer Programming, 11(1), October 1988. lso reprinted in [121].

    Google Scholar 

  117. C. Carroll Morgan. The specification statement. ACM Transactions on Programming Languages and Systems (TOPLAS), 10(3), July 1988. lso reprinted in [121].

    Google Scholar 

  118. C. Carroll Morgan. Types and invariants in the refinement calculus. In Proc. Mathematics of Program Construction Conference, June 1989.

    Google Scholar 

  119. C. Carroll Morgan. Programming from Specifications. International Series in Computer Science. Prentice Hall, Hemel Hempstead, Hertfordshire HP2 4RG, UK, 1990.

    Google Scholar 

  120. C. Carroll Morgan and Ken A. Robinson. Specification statements and refinement. IBM Journal of Research and Development, 31(5), September 1987. Also reprinted in [121].

    Google Scholar 

  121. C. Carroll Morgan, Ken A. Robinson, and Paul H.B. Gardiner. On the refinement calculus. Technical Monograph PRG-70, Oxford University Computing Laboratory, 11 Keble Road, Oxford, UK, October 1988.

    Google Scholar 

  122. C. Carroll Morgan and Jeff W. Sanders. Laws of the logical calculi. Technical Monograph PRG-78, Oxford University Computing Laboratory, 11 Keble Road, Oxford, UK, September 1989. This document records some important laws of classical predicate logic. It is designed as a reservoir to be tapped by users of logic, in system development.

    Google Scholar 

  123. C. Carroll Morgan and Bernard A. Sufrin. Specification of the Unix filing system. IEEE Transactions on Software Engineering, 10 (2): 128–142, March 1984.

    MATH  Google Scholar 

  124. P. Mundy and John B. Wordsworth. The CICS application programming interface: Transient data and storage control. IBM Technical Report TR12.299, IBM United Kingdom Laboratories Ltd., Hursley Park, Winchester, Hampshire 5021 2JN, UK, October 1990. One of a number of reports on the CICS application programming interface. See also [16, 86, 99].

    Google Scholar 

  125. K.T. Narayana and Sanjeev Dharap. Formal specification of a look manager. IEEE Transactions on Software Engineering, 16(9):1089–1103, September 1990. A formal specification of the look manager of a dialog system is presented in Z. This deals with the presentation of visual aspects of objects and the editing of those visual aspects.

    Google Scholar 

  126. K.T. Narayana and Sanjeev Dharap. Invariant properties in a dialog system. ACM SIGSOFT Software Engineering Notes, 15 (4): 67–79, September 1990.

    Article  Google Scholar 

  127. T.C. Nash. Using Z to describe large systems. In John E. Nicholls, editor, Z User Workshop, Oxford 1989, Workshops in Computing, pages 150–178. Springer-Verlag, 1990.

    Google Scholar 

  128. Dave Neilson. Hierarchical refinement of a Z specification. In Proc. Foundations of Software Technology and Theoretical Computer Science, December 1987.

    Google Scholar 

  129. John E. Nicholls. Working with formal methods. Journal of Information Technology, 2 (2): 67–71, June 1987.

    Article  Google Scholar 

  130. John E. Nicholls, editor. Z in the Development Process, Oxford, UK, June 1989. Oxford University Computing Laboratory. Proceedings of a discussion workshop held on Thursday 15 December in Oxford, UK, with contributions by Peter Collins, David Cooper, Anthony Hall, Patrick Hall, Brian Hepworth, Ben Potter and Andrew Ricketts. It is available from the Librarian at the PRG.

    Google Scholar 

  131. John E. Nicholls, editor. Z User Workshop, Oxford 1989, Workshops in Computing. Springer-Verlag, 1990. Proceedings of the Fourth Annual Z User Meeting, 15 December 1989, Oxford, UK. Published in collaboration with the British Computer Society. For the opening address see [134]. For individual papers, see [11, 29, 30, 41, 45, 58, 68, 81, 84, 92, 105, 127, 135, 152, 163, 178].

    Google Scholar 

  132. C.J. Nix and B.P. Collins. The use of software engineering, including the Z notation, in the development of CICS. Quality Assurance, 14 (3): 103–110, September 1988.

    Google Scholar 

  133. M. Norris. Z — a rigorous system specification technique. STARTS debrief report, The National Computing Centre Ltd., Oxford Road, Manchester M1 7ED, UK, 1986. Other reports in the series include: SLIM, PRICE S, ARTEMIS, VDM, SOFCHIP, JSD, SDL, SAFRA and CORE.

    Google Scholar 

  134. Brian Oakley. The state of use of formal methods. In John E. Nicholls, editor, Z User Workshop, Oxford 1989, Workshops in Computing, pages 1–5. Springer-Verlag, 1990. A record of the opening address at the meeting.

    Google Scholar 

  135. M. Philips. CICS/ESA 3.1 experiences. In John E. Nicholls, editor, Z User Workshop, Oxford 1989, Workshops in Computing, pages 179–185. Springer-Verlag, 1990.

    Google Scholar 

  136. Michael Pilling, Alan Burns, and Kerry Raymond. Formal specifications and proofs of inheritance protocols for real-time scheduling. Software Engineering Journal, 5 (5): 263–279, September 1990.

    Article  Google Scholar 

  137. Ben F. Potter, Jane E. Sinclair, and David Till. An Introduction to Formal Specification and Z. International Series in Computer Science. Prentice Hall, Hemel Hempstead, Hertfordshire HP2 4RG, UK, 1990.

    Google Scholar 

  138. Gill P. Randell. Translating data flow diagrams into Z (and vice versa). RSRE Report no. 90019, Royal Signals and Radar Establishment, Ministry of Defence, Malvern, UK, 1990.

    Google Scholar 

  139. Joy N. Reed. Semantics-based tools for a specification support environment. In Mathematical Foundations of Programming Language Semantics, volume 298 of Lecture Notes in Computer Science. Springer-Verlag, 1988.

    Google Scholar 

  140. Joy N. Reed and Jane E. Sinclair. An algorithm for type-checking Z: A Z specification. Technical Monograph PRG-81, Oxford University Computing Laboratory, 11 Keble Road, Oxford, UK, March 1990.

    Google Scholar 

  141. Gordon A. Rose and Peter Robinson. A case study in formal specifications. In Proc. First Australian Software Engineering Conference, May 1986.

    Google Scholar 

  142. Augusto Sampaio and S. Meira. Modular extensions to Z. In D. Bjorner, C.A.R. Hoare, and H. Langmaack, editors, VDM and Z — Formal Methods in Software Development, volume 428 of Lecture Notes in Computer Science, pages 211–232. VDM-Europe, Springer-Verlag, 1990.

    Chapter  Google Scholar 

  143. Lesley T. Semmens and Pat M. Allen. Using entity relationship models as a basis for Z specifications. Technical Report IES1/90, Leeds Polytechnic, Faculty of Information and Engineering Systems, Leeds, UK, 1990.

    Google Scholar 

  144. Lesley T. Semmens and Pat M. Allen. Using Yourdon and Z to specify computer security: A case study. Technical Report IES4/90, Leeds Polytechnic, Faculty of Information and Engineering Systems, Leeds, UK, 1990.

    Google Scholar 

  145. Chris T. Sennett. A combined security and integrity policy model appendix to development environment for secure software. RSRE Report no. 87015, Royal Signals and Radar Establishment, Ministry of Defence, Malvern, UK, November 1987. 368

    Google Scholar 

  146. Chris T. Sennett. Review of type checking and scope rules of the specification language Z. RSRE Report no. 87017, Royal Signals and Radar Establishment, Ministry of Defence, Malvern, UK, November 1987.

    Google Scholar 

  147. Chris T. Sennett and Ruaridh Macdonald. Separability and security models. RSRE Report no. 87020, Royal Signals and Radar Establishment, Ministry of Defence, Malvern, UK, November 1987.

    Google Scholar 

  148. David E. Shepherd. Verified microcode design. Microprocessors and Microsystems, 14(10):623–630, December 1990. This article shows how high-level Occam was transformed to a low level implementation that matched the micromachine functions of the T800 transputer in order to verify its microcode. The high-level specification is first given in Z. The article is part of a special issue on Formal aspects of microprocessor design, edited by Hussein Zedan. See also [24].

    Google Scholar 

  149. David E. Shepherd and Greg Wilson. Making chips that work. New Scientist, 1664:61–64, May 1989. A general article containing information on the formal development of the T800 floating-point unit for the transputer including the use of Z.

    Google Scholar 

  150. Lewis N. Simcox. The application of Z to the specification of air traffic control systems: 1. RSRE Memorandum no. 4280, Royal Signals and Radar Establishment, Ministry of Defence, Malvern, UK, April 1989.

    Google Scholar 

  151. Alf Smith. The Knuth-Bendix completion algorithm and its specification in Z. RSRE Memorandum no. 4323, Royal Signals and Radar Establishment, Ministry of Defence, Malvern, UK, September 1989.

    Google Scholar 

  152. Alf Smith. The Knuth-Bendix completion algorithm and its specification in Z. In John E. Nicholls, editor, Z User Workshop, Oxford 1989, Workshops in Computing, pages 195–220. Springer-Verlag, 1990.

    Google Scholar 

  153. Graeme Smith and Roger Duke. Specification and verification of a cache coherence protocol. Technical Report 126, Department of Computer Science, University of Queensland, Australia, 1989.

    Google Scholar 

  154. Graeme Smith and Roger Duke. Modelling a cache coherence protocol using Object-Z. In Proc. 13th Australian Computer Science Conference (ACSC-13), pages 352–361, 1990.

    Google Scholar 

  155. Ib H. Sorensen. A specification language. In J. Staunstrup, editor, Program Specification: Proceedings of a Workshop, volume 134 of Lecture Notes in Computer Science, pages 381–401. Springer-Verlag, 1981.

    Google Scholar 

  156. J. Michael Spivey. The fuzz Manual. Computing Science Consultancy, 2 Willow Close, Garsington, Oxford OX9 9AN, UK, 1988. A Z type-checker and fuzz. sty style option for LATEX documents [104]. The package is compatible with the book, The Z Notation: A Reference Man ual by the same author [159]. Send orders to Mrs. A. Spivey, 34 Westlands Grove, Stockton Lane, York YO3 OEF. Technical enquiries can be sent to Mike Spivey at 2 Willow Close, Garsington, Oxford OX9 9AN, or by e-mail at Cost: SUN 3 or SUN 4 version on cartridge tape, f300, or on 3.5in disk, f275, and IBM PC version on 5.25in or 3.5in disk, f200. Cheques should be made payable to Dr. J.M. Spivey.

    Google Scholar 

  157. J. Michael Spivey. Understanding Z: A Specification Language and its Formal Semantics, volume 3 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, UK, January 1988. Published version of 1985 DPhil thesis.

    Google Scholar 

  158. J. Michael Spivey. An introduction to Z and formal specifications. Software Engineering Journal, 4 (1), January 1989.

    Google Scholar 

  159. J. Michael Spivey. The Z Notation: A Reference Manual. International Series in Computer Science. Prentice Hall, Hemel Hempstead, Hertfordshire HP2 4RG, UK, 1989. This book is currently the de facto standard for the Z notation.

    Google Scholar 

  160. J. Michael Spivey. A guide to the zed style option. Oxford University Computing Laboratory, December 1990. A description of the Z style option zed. sty for use with the LATEX document preparation system [104]. The style file and the guide are available electronically by sending an e-mail message

    Google Scholar 

  161. J. Michael Spivey. Specifying a real-time kernel. IEEE Software, pages 21–28, September 1990. This case study of an embedded real-time kernel shows that mathematical techniques have an important role to play in documenting systems and avoiding design flaws.

    Google Scholar 

  162. J. Michael Spivey and Bernard A. Sufrin. Type inference in Z. In D. Bjorner, C.A.R. Hoare, and H. Langmaack, editors, VDM and Z - Formal Methods in Software Development, volume 428 of Lecture Notes in Computer Science, pages 426–438. VDM-Europe, Springer-Verlag, 1990. See also [163].

    Google Scholar 

  163. J. Michael Spivey and Bernard A. Sufrin. Type inference in Z. In John E. Nicholls, editor, Z User Workshop, Oxford 1989, Workshops in Computing, pages 6–31. Springer-Verlag, 1990.

    Google Scholar 

  164. Susan Stepney and Stephen P. Lord. Formal specification of an access control system. Software–Practice and Experience, 17 (9): 575–593, September 1987.

    Article  Google Scholar 

  165. Bernard A. Sufrin. Formal specification of a display editor. Technical Monograph PRG-21, Oxford University Computing Laboratory, 11 Keble Road, Oxford, UK, June 1981. Out of print.

    Google Scholar 

  166. Bernard A. Sufrin. Formal specification: Notation and examples. In D. Neel, editor, Tools and Notations for Program Construction Cambridge University Press, UK, 1982. Example of a filing system specification, first published use of the schema notation to put together states.

    Google Scholar 

  167. Bernard A. Sufrin. Towards formal specification of the ICL data dictionary. ICL Technical Journal, August 1984.

    Google Scholar 

  168. Bernard A. Sufrin. Formal methods and the design of effective user interfaces. In M.D. Harrison and A.F. Monk, editors, People and Computers: Designing for Usability. Cambridge University Press, UK, 1986.

    Google Scholar 

  169. Bernard A. Sufrin. Using the Hippo system. Oxford University Computing Laboratory, 1989. Hippo is a Z type-checker written in New Jersey Standard ML. It is a successor to the Zebra and Forsite type-checkers. Copies are available by sending a SUN cartridge tape to the author.

    Google Scholar 

  170. Bernard A. Sufrin and James C.P. Woodcock. Towards the formal specification of a simple programming support environment. Software Engineering Journal, 2 (4): 86–94, July 1987.

    Article  Google Scholar 

  171. Phil F. Terry and Simon R. Wiseman. On the design and implementation of a secure computer system. RSRE Memorandum no. 4188, Royal Signals and Radar Establishment, Ministry of Defence, Malvern, UK, June 1988.

    Google Scholar 

  172. David Till and Ben F. Potter. The specification in Z of gateway functions within a communications network. In Proc. IFIP WG10.3 Conference on Distributed Processing, Amsterdam, The Netherlands, October 1897. Elsevier Science Publishers B.V. (North-Holland).

    Google Scholar 

  173. Brian S. Todd. A model-based diagnostic program. Software Engineering Journal, 2 (3): 54–63, May 1987.

    Article  Google Scholar 

  174. Ian Toyn. CADiZ Quick Reference Guide. York Software Engineering Ltd., 1990. A guide to the CADiZ (Computer Aided Design in Z) toolkit. This makes use of the UNIX troff family of text formatting tools.

    Google Scholar 

  175. Ian Toyn and John A. McDermid. Zork: A type-checker for Z from York. In Colloquium on The Application of CASE Tools, Digest No: 1990/058. The Institution of Electrical Engineers, April 1990. Zork has now been renamed CADiZ [174].

    Google Scholar 

  176. M.J. van Diepen and K.M. van Hee. A formal semantics for Z and the link between Z and the relational algebra. In D. Bjorner, C.A.R. Hoare, and H. Langmaack, editors, VDM and Z–Formal Methods in Software Development, volume 428 of Lecture Notes in Computer Science, pages 526–551. VDM-Europe, Springer-Verlag, 1990.

    Chapter  Google Scholar 

  177. Martin Ward. From assembler to Z using formal transformations. Centre for Software Maintenance, University of Durham, UK, 1989.

    Google Scholar 

  178. Robin W. Whitty. Structural metrics for Z specifications. In John E. Nicholls, editor, Z User Workshop, Oxford 1989, Workshops in Computing, pages 186 191. Springer-Verlag, 1990.

    Google Scholar 

  179. P.J. Whysall and John A. McDermid. Object oriented specification and refinement. In Proceedings of the 4th Refinement Workshop. Springer-Verlag, 1991. To appear.

    Google Scholar 

  180. Jeannette M. Wing. A specifiers introduction to formal methods. IEEE Computer, September 1990.

    Google Scholar 

  181. Simon R. Wiseman and Clare L. Harrold. A security model and its implementation. RSRE Memorandum no. 4222, Royal Signals and Radar Establishment, Ministry of Defence, Malvern, UK, September 1988.

    Google Scholar 

  182. Andrew W. Wood. A Z specification of the MaCHO interface editor. RSRE Memorandum no. 4247, Royal Signals and Radar Establishment, Ministry of Defence, Malvern, UK, November 1988.

    Google Scholar 

  183. William G. Wood. Application of formal methods to system and software specification. ACM SIGSOFT Software Engineering Notes, 15 (4): 144–146, September 1990.

    Google Scholar 

  184. James C.P. Woodcock. Teaching how to use mathematics for large-scale software development. Bull. BCS-FACS, July 1988.

    Google Scholar 

  185. James C.P. Woodcock. The applicability of formal methods. In Proc. Halifax Formal Methods Workshop, 1989.

    Google Scholar 

  186. James C.P. Woodcock. Calculating properties of Z specifications. ACM SIG-SOFT Software Engineering Notes, 14 (4): 43–54, 1989.

    Article  Google Scholar 

  187. James C.P. Woodcock. Mathematics as a management tool: Proof rules for promotion. In Proc. 6th Annual CSR Conference on Large Software Systems, September 1989.

    Google Scholar 

  188. James C.P. Woodcock. Parallel refinement in Z. In Proc. Workshop on Refinement. Butterworths, January 1989.

    Google Scholar 

  189. James C.P. Woodcock. Structuring specifications in Z. Software Engineering Journal, 4 (1): 51–66, January 1989.

    Article  Google Scholar 

  190. James C.P. Woodcock. Transaction refinement in Z. In Proc. Workshop on Refinement. Butterworths, January 1989.

    Google Scholar 

  191. James C.P. Woodcock. Z. In Proc. Halifax Formal Methods Workshop, 1989.

    Google Scholar 

  192. James C.P. Woodcock. Using Z - Specification, Refinement and Proof. Oxford University Computing Laboratory, 11 Keble Road, Oxford, UK, 1991. In preparation.

    Google Scholar 

  193. James C.P. Woodcock and Martin Loomes. Software Engineering Mathematics: Formal Methods Demystified. Pitman Publishing Ltd., London, UK, 1988.

    Book  Google Scholar 

  194. James C.P. Woodcock and C. Carroll Morgan. Refinement of state-based concurrent systems. In D. Bjorner, C.A.R. Hoare, and H. Langmaack, editors, VDM and Z–Formal Methods in Software Development, volume 428 of Lecture Notes in Computer Science, pages 340–351. VDM-Europe, Springer-Verlag, 1990. Work on combining Z and CSP.

    Chapter  Google Scholar 

  195. John B. Wordsworth. Teaching formal specification methods in an industrial environment. In Proc. Software Engineering 86, London, UK, 1986. IEE/BCS, Peter Peregrinus.

    Google Scholar 

  196. John B. Wordsworth. Specifying and refining programs with Z. In Proc. Second IEE/BCS Conference on Software Engineering, volume 290, pages 8–16. IEE/BCS, July 1988. A tutorial summary.

    Google Scholar 

  197. John B. Wordsworth. Refinement tutorial: A storage manager. In Proc. Workshop on Refinement. Butterworths, January 1989.

    Google Scholar 

  198. John B. Wordsworth. A Z development method. In Proc. Workshop on Refinement. Butterworths, January 1989.

    Google Scholar 

  199. William D. Young. Comparing specifications paradigms: Gypsy and Z. Technical Report 45, Computational Logic Inc., 1717 W. 6th St., Suite 290, Austin, Texas 78703, USA, 1989. Presented at the 12th National Computer Security Conference, Baltimore, Maryland, USA, 10–13 October 1989.

    Google Scholar 

  200. PRG archive server. Oxford University Computing Laboratory, 1991. A computer-based archive server at the Programming Research Group in Oxford is available for use by anyone with access to electronic mail. This allows people interested in Z (and other things) to access various archived files. In particular, back issues of the Z FORUM electronic newsletter [201] and a Z bibliography [25] are available. To access the archive server, send

    Google Scholar 

  201. vol. 5.1–5.3 (1990). Z FORUM is a moderated electronic mailing list. It was initiated as a newsletter by Ruaridh Macdonald of RSRE, Malvern, and is now maintained by Jonathan Bowen at the PRG. Contributions should be sent to the moderator via Requests to join or leave the list should be sent to Messages are now forwarded to the list directly to ensure timeliness. A list of back issues of newsletters and other Z-related material is also available via email by sending a message of index z to the PRG archive server [200] on For a particular issue, send a message such as send z 5. 3.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Programming Research Group, Oxford University Computing Laboratory, 11 Keble Road, Oxford, OX1 3QD, UK

    Jonathan Bowen

Authors
  1. Jonathan Bowen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Programming Research Group, Oxford University Computing Laboratory, 8-11 Keble Road, OX1 3QD, Oxford, UK

    J. E. Nicholls MA

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bowen, J. (1991). Selected Z Bibliography. In: Nicholls, J.E. (eds) Z User Workshop, Oxford 1990. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3540-1_23

Download citation

  • DOI: https://doi.org/10.1007/978-1-4471-3540-1_23

  • Publisher Name: Springer, London

  • Print ISBN: 978-3-540-19672-3

  • Online ISBN: 978-1-4471-3540-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation