Selected Z Bibliography

  • Jonathan Bowen
Conference paper
Part of the Workshops in Computing book series (WORKSHOPS COMP.)

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).

Keywords

Europe Radar Coherence Nash Editing 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [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. [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. [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. [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. [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, 1981Google Scholar
  6. [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. [7]
    M. Bailey. Formal specification using Z. In Proc. Software Engineering anniversary meeting (SEAS), page 99. SEA, 1987.Google Scholar
  8. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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 commandGoogle Scholar
  20. [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. [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 viaGoogle Scholar
  22. [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. [23]
    Jonathan P. Bowen. POS: Formal specification of a UNIX tool. Software Engineering Journal, 4 (1): 67–72, January 1989.CrossRefGoogle Scholar
  24. [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. [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 possibleGoogle Scholar
  26. [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. [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. [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. [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. [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. [31]
    Alan Burns and I.W. Morrison. A formal description of the structure attribute model. Software Engineering Journal, 4 (2): 74–78, March 1989.CrossRefGoogle Scholar
  32. [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. [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. [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. [35]
    Paul Butcher. A behavioural semantics for Linda-2. Department of Computer Science, University of York, 1990.Google Scholar
  36. [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. [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. [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.CrossRefGoogle Scholar
  39. [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.CrossRefGoogle Scholar
  40. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [55]
    Roger Duke and Graeme Smith. Temporal logic and Z specifications. Australian Computer Journal, 21 (2): 62–66, May 1989.Google Scholar
  56. [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. [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. [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. [59]
    David Garlan. The role of reusable frameworks. ACM SIGSOFT Software Engineering Notes, 15 (4): 42–44, September 1990.CrossRefGoogle Scholar
  60. [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.CrossRefGoogle Scholar
  61. [61]
    Susan L. Gerhart. Applications of formal methods: Developing virtuoso software. IEEE Software, pages 6–10, September 1990.Google Scholar
  62. [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. [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. [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. [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. [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.CrossRefGoogle Scholar
  67. [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.CrossRefGoogle Scholar
  68. [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. [69]
    Frank Halasz and Mayer Schwartz. The Dexter hypertext reference model. In NIST Hypertext Standardization Workshop, January 1990.Google Scholar
  70. [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. [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.CrossRefGoogle Scholar
  72. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [82]
    Ian J. Hayes. Specification of an oscilloscope. Department of Computer Science, University of Queensland, 1990.Google Scholar
  83. [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. [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. [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. [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. [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. [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. [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. [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. [91]
    Jonathan Jacky. Formal specifications for a clinical cyclotron control system. ACM SIGSOFT Software Engineering Notes, 15 (4): 45–54, September 1990.CrossRefGoogle Scholar
  92. [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. [93]
    P. Johnson. Using Z to specify CICS. In Proc. Software Engineering anniversary meeting (SEAS), page 303. SEA, 1987.Google Scholar
  94. [94]
    Mark Josephs. The data refinement calculator for Z specifications. Information Processing Letters, 27 (1): 29–33, 1988.MathSciNetCrossRefGoogle Scholar
  95. [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. [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. [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. [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 sendingGoogle Scholar
  99. [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. [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.CrossRefGoogle Scholar
  101. [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. [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. [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. [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. [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. [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. [107] Ralph L. London and Kathleen R. Milsted. Specifying and verifying reusable components using Z: Sets and dictionaries. Technical Report CR-88-10, Tektronix Laboratories, P.O. Box 500, MS 50-662, Beaverton, Oregon 97077, USA, October 1988. shortened version [108]
    is also in the Proceedings of the Fifth International Workshop on Software Specification and Design, Pittsburgh, Pennsylvania, 19–20 May 1989.Google Scholar
  108. [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. [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. [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. [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. [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. [113]
    B. Meyer. On formalism in specifications. IEEE Software, 2 (1): 6–26, January 1985.CrossRefGoogle Scholar
  114. [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. [115]
    C. Carroll Morgan. Data refinement using miracles. Information Processing Letters, 26(5):243–246, January 1988. lso reprinted in [121].Google Scholar
  116. [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. [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. [118]
    C. Carroll Morgan. Types and invariants in the refinement calculus. In Proc. Mathematics of Program Construction Conference, June 1989.Google Scholar
  119. [119]
    C. Carroll Morgan. Programming from Specifications. International Series in Computer Science. Prentice Hall, Hemel Hempstead, Hertfordshire HP2 4RG, UK, 1990.Google Scholar
  120. [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. [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. [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. [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.MATHGoogle Scholar
  124. [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. [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. [126]
    K.T. Narayana and Sanjeev Dharap. Invariant properties in a dialog system. ACM SIGSOFT Software Engineering Notes, 15 (4): 67–79, September 1990.CrossRefGoogle Scholar
  127. [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. [128]
    Dave Neilson. Hierarchical refinement of a Z specification. In Proc. Foundations of Software Technology and Theoretical Computer Science, December 1987.Google Scholar
  129. [129]
    John E. Nicholls. Working with formal methods. Journal of Information Technology, 2 (2): 67–71, June 1987.CrossRefGoogle Scholar
  130. [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. [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. [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. [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. [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. [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. [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.CrossRefGoogle Scholar
  137. [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. [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. [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. [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. [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. [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.CrossRefGoogle Scholar
  143. [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. [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. [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. 368Google Scholar
  146. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [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. [158]
    J. Michael Spivey. An introduction to Z and formal specifications. Software Engineering Journal, 4 (1), January 1989.Google Scholar
  159. [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. [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 messageGoogle Scholar
  161. [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. [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. [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. [164]
    Susan Stepney and Stephen P. Lord. Formal specification of an access control system. Software–Practice and Experience, 17 (9): 575–593, September 1987.CrossRefGoogle Scholar
  165. [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. [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. [167]
    Bernard A. Sufrin. Towards formal specification of the ICL data dictionary. ICL Technical Journal, August 1984.Google Scholar
  168. [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. [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. [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.CrossRefGoogle Scholar
  171. [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. [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. [173]
    Brian S. Todd. A model-based diagnostic program. Software Engineering Journal, 2 (3): 54–63, May 1987.CrossRefGoogle Scholar
  174. [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. [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. [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.CrossRefGoogle Scholar
  177. [177]
    Martin Ward. From assembler to Z using formal transformations. Centre for Software Maintenance, University of Durham, UK, 1989.Google Scholar
  178. [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. [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. [180]
    Jeannette M. Wing. A specifiers introduction to formal methods. IEEE Computer, September 1990.Google Scholar
  181. [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. [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. [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. [184]
    James C.P. Woodcock. Teaching how to use mathematics for large-scale software development. Bull. BCS-FACS, July 1988.Google Scholar
  185. [185]
    James C.P. Woodcock. The applicability of formal methods. In Proc. Halifax Formal Methods Workshop, 1989.Google Scholar
  186. [186]
    James C.P. Woodcock. Calculating properties of Z specifications. ACM SIG-SOFT Software Engineering Notes, 14 (4): 43–54, 1989.CrossRefGoogle Scholar
  187. [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. [188]
    James C.P. Woodcock. Parallel refinement in Z. In Proc. Workshop on Refinement. Butterworths, January 1989.Google Scholar
  189. [189]
    James C.P. Woodcock. Structuring specifications in Z. Software Engineering Journal, 4 (1): 51–66, January 1989.CrossRefGoogle Scholar
  190. [190]
    James C.P. Woodcock. Transaction refinement in Z. In Proc. Workshop on Refinement. Butterworths, January 1989.Google Scholar
  191. [191]
    James C.P. Woodcock. Z. In Proc. Halifax Formal Methods Workshop, 1989.Google Scholar
  192. [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. [193]
    James C.P. Woodcock and Martin Loomes. Software Engineering Mathematics: Formal Methods Demystified. Pitman Publishing Ltd., London, UK, 1988.CrossRefGoogle Scholar
  194. [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.CrossRefGoogle Scholar
  195. [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. [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. [197]
    John B. Wordsworth. Refinement tutorial: A storage manager. In Proc. Workshop on Refinement. Butterworths, January 1989.Google Scholar
  198. [198]
    John B. Wordsworth. A Z development method. In Proc. Workshop on Refinement. Butterworths, January 1989.Google Scholar
  199. [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. [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, sendGoogle Scholar
  201. [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

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • Jonathan Bowen
    • 1
  1. 1.Programming Research GroupOxford University Computing LaboratoryOxfordUK

Personalised recommendations