Skip to main content
SpringerLink
Log in

The use of Z

  • Conference paper
Z User Workshop, York 1991

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

Abstract

During 1990 and 1991 we carried out a survey of Z users in the UK; in this paper we present the results. Z is being used by a wide variety of companies for many different applications. Many institutions use Z because they choose to, rather than because it is mandated by a defence or security related client. Half of the participants in the survey were first- time users of Z; with a little training and some expert guidance they were soon able to produce Z specifications. Nearly all the institutions who have used Z intend to do so again; those who don’t plan to use a formal method more appropriate to their needs. We did not uncover many really large projects using Z, but most of those which we did survey are of a reasonable size. Over half the projects surveyed are using tools, with the majority of them employing type checking support. Tools use grows with the size of the project, although several large specifications have been produced without the use of tools. Not many people are proving their specifications, nor stating desirable theorems or proof obligations. However, many people expressed an interest in this with the unavailability of appropriate tool support being given as a reason for not attempting proof.

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.

Similar content being viewed by others

Bibliography

  1. Jean-Raymond Abrial. A refinement case study (using the Abstract Machine Notation). In Joseph M. Morris and Roger C. Shaw, editors, 4th Refinement Workshop, Workshops in Computing, pages 51–96. Springer Verlag, 1991.

    Google Scholar 

  2. Rosalind Barden, Susan Stepney, and David Cooper. Report of a survey into the use of Z. ZIP document ZIP/Logica/91/094, Logica Cambridge Ltd., December 1991.

    Google Scholar 

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

    Article  Google Scholar 

  4. David Brownbridge. Using Z to develop a CASE toolset. In [Nicholls 1990], pages 142–149.

    Google Scholar 

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

    Google Scholar 

  6. R. M. Gallimore, D. Coleman, and V. Stavridou. UMIST OBJ: a language for executable program specifications. The Computer Journal, 32(5): 413–421, 1989.

    Article  Google Scholar 

  7. C. Gane and T. Sarson. Structured Systems Analysis: Tools and Techniques. Prentice Hall, 1979.

    Google Scholar 

  8. David Garlan and Norman Delisle. Formal specifications as reusable frameworks. In Dines Bjørner, C. A. R. Hoare, and H. Langmaack, editors, VDM’90: VDM and Z — Formal Methods in Software Development, Kiel, volume 428 of Lecture Notes in Computer Science, pages 150–163. Springer Verlag, 1990.

    Google Scholar 

  9. C. W. George and Robert E. Milne. Specifying and refining concurrent systems — an example from the RAISE project. In C. Carroll Morgan and James C. P. Woodcock, editors, Third BCS-FACS Refinement Workshop, Workshops in Computing, pages 155–168. Springer Verlag, 1991.

    Google Scholar 

  10. Joseph A. Goguen and Timothy Winkler. Introducing OBJ3. Technical Report SRI-CSL-88-9, SRI International, 1988.

    Google Scholar 

  11. Michael J. C. Gordon. HOL: A machine oriented formulation of higher order logic. Technical Report 68, University of Cambridge, 1985.

    Google Scholar 

  12. J. V. Guttag, J. J. Horning, and Jeannette M. Wing. The Larch family of specification languages. IEEE Software, 2(5): 24–36, 1985.

    Article  Google Scholar 

  13. J. V. Guttag, J. J. Horning, and Jeannette M. Wing. Larch in five easy pieces. Technical report, Digital Systems Research Center, July 1985.

    Google Scholar 

  14. J. Anthony Hall. Seven myths of formal methods. IEEE Software, pages 21–28, September 1990.

    Google Scholar 

  15. C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.

    Google Scholar 

  16. ISO/TC97/SC21. LOTOS, a formal description technique based on the temporal ordering of observational behaviour. Draft International Standard ISO/DIS/8807, International Standards Organization, 1987.

    Google Scholar 

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

    Google Scholar 

  18. Cliff B. Jones. Systematic Software Development using VDM. Prentice Hall, 1986.

    Google Scholar 

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

    Google Scholar 

  20. Stephen J. Mellor and P. T. Ward. Structured Development for Real Time Systems. Yourdon Press, 1985, 1986. 3 volumes.

    Google Scholar 

  21. Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer Verlag, 1980.

    Google Scholar 

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

    Google Scholar 

  23. G. Mullery. CORE — a method for controlled requirement specification. In Proceedings of the 4th International Conference on Software Engineering, Munich, pages 126–135, 1979.

    Google Scholar 

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

    Google Scholar 

  25. John E. Nicholls, editor. Z User Workshop: Proceedings of the Fourth Annual Z User Meeting, Oxford, Workshops in Computing. Springer Verlag, 1990.

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  28. Mark Phillips. CICS/ESA 3.1 experiences. In [Nicholls 1990], pages 179–185.

    Google Scholar 

  29. Lesley Semmens and Pat Allen. Using Yourdon and Z: An approach to formal specification. In John E. Nicholls, editor, Proceedings of the Fifth Annual Z User Meeting, Oxford, Workshops in Computing, pages 228–253. Springer Verlag, 1991.

    Google Scholar 

  30. David Shepherd and Greg Wilson. Making chips that work. New Scientist, 1664: 61–64, May 1989.

    Google Scholar 

  31. J. Michael Spivey. The Z Notation: a Reference Manual. Prentice Hall, 1989.

    Google Scholar 

  32. Manchester NCC. SSADM Manual Version 3, 1986.

    Google Scholar 

  33. Manchester NCC. SSADM Manual Version 4, 1990.

    Google Scholar 

  34. Susan Stepney, Rosalind Barden, and David Cooper. Comparative study of object orientation in Z. ZIP document ZIP/Logica/90/046(3), Logica Cambridge Ltd., December 1991.

    Google Scholar 

  35. Susan Stepney, Rosalind Barden, and David Cooper. A survey of object orientation in Z. IEE Software Engineering Journal, March 1992.

    Google Scholar 

  36. Edward Yourdon and L. L. Constantine. Structured Design: Fundamentals of a Discipline of Computer Program and Systems Design. Yourdon Press, 2nd edition, 1978.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Logica Cambridge Ltd, Betjeman House, 104 Hills Road, Cambridge, CB2 1LQ, UK

    Rosalind Barden, Susan Stepney & David Cooper

Authors
  1. Rosalind Barden
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Susan Stepney
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. David Cooper
    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, Oxford, 0X1 3QD, UK

    J. E. Nicholls MA

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Logica UK Ltd

About this paper

Cite this paper

Barden, R., Stepney, S., Cooper, D. (1991). The use of Z. In: Nicholls, J.E. (eds) Z User Workshop, York 1991. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3203-5_5

Download citation

  • DOI: https://doi.org/10.1007/978-1-4471-3203-5_5

  • Publisher Name: Springer, London

  • Print ISBN: 978-3-540-19780-5

  • Online ISBN: 978-1-4471-3203-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation