Skip to main content
SpringerLink
Log in

An Introduction to Z

  • Chapter
Refinement in Z and Object-Z

  • 945 Accesses

Abstract

This chapter introduces the Z specification notation. Z is a formal specification language. It is a language in that it provides a notation for describing the behaviour of a system, and it is formal in that it uses mathematics to do so. The mathematics is simple, consisting of first order predicate logic and set theory. However, based upon this, it offers a very elegant way of structuring the mathematics to provide a specification of the system under consideration. In this chapter we present the notations for logic, sets and relations, the schema notation and the schema calculus, leading to the definition of an abstract data type in the “states-and-operations” style, and the first example refinement.

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 84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 109.99
Price excludes VAT (USA)
  • Durable hardcover 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

Notes

  1. 1.

    The symbol ∅ is overloaded, denoting the empty sets of all possible types.

  2. 2.

    Representing only very partial information about which player has ever played for which club.

  3. 3.

    In graphical presentations of expressions returning schemas, we often put the expression in place of the name. This is done purely for presentational purposes, as expressions denote unnamed schemas.

  4. 4.

    Note that this is a refinement example, not an example of good programming practice!

  5. 5.

    However, Object-Z does have such a semantics.

References

  1. Araki, K., Gnesi, S., & Mandrioli, D. (Eds.) (2003). Formal Methods Europe (FME 2003). Lecture Notes in Computer Science: Vol. 2805. Berlin: Springer.

    MATH  Google Scholar 

  2. Arthan, R. D. (1991). On free type definitions in Z. In J. E. Nicholls (Ed.), Sixth Annual Z User Workshop (pp. 40–58). Berlin: Springer.

    Google Scholar 

  3. Barden, R., Stepney, S., & Cooper, D. (1994). Z in Practice. BCS Practitioner Series. New York: Prentice Hall.

    MATH  Google Scholar 

  4. Bert, D., Bowen, J. P., Henson, M. C., & Robinson, K. (Eds.) (2002). ZB 2002: Formal Specification and Development in Z and B, 2nd International Conference of B and Z Users. Lecture Notes in Computer Science: Vol. 2272. Berlin: Springer.

    Google Scholar 

  5. Bert, D., Bowen, J. P., King, S., & Waldén, M. A. (Eds.) (2003). ZB 2003: Formal Specification and Development in Z and B, Third International Conference of B and Z Users. Lecture Notes in Computer Science: Vol. 2651. Berlin: Springer.

    Google Scholar 

  6. Boiten, E. A., Derrick, J., & Schellhorn, G. (2009). Relational concurrent refinement II: internal operations and outputs. Formal Aspects of Computing, 21(1–2), 65–102.

    Article  MATH  Google Scholar 

  7. Börger, E., Butler, M. J., Bowen, J. P., & Boca, P. (Eds.) (2008). ABZ 2008. Lecture Notes in Computer Science: Vol. 5238. Berlin: Springer.

    MATH  Google Scholar 

  8. Bottaci, L., & Jones, J. (1995). Formal Specification Using Z: A Modelling Approach. International Thomson Publishing.

    Google Scholar 

  9. Bowen, J. P. (1996). Formal Specification and Documentation Using Z: A Case Study Approach. International Thomson Computer Press.

    Google Scholar 

  10. Bowen, J. P., Dunne, S., Galloway, A., & King, S. (Eds.) (2000). ZB2000: Formal Specification and Development in Z and B. Lecture Notes in Computer Science: Vol. 1878. Berlin: Springer.

    Google Scholar 

  11. Bowen, J. P., Fett, A., & Hinchey, M. G. (Eds.) (1998). ZUM’98: The Z Formal Specification Notation. Lecture Notes in Computer Science: Vol. 1493. Berlin: Springer.

    Google Scholar 

  12. Bowen, J. P., & Hall, J. A. (Eds.) (1994). ZUM’94, Z User Workshop. Workshops in Computing. Cambridge: Springer.

    Google Scholar 

  13. Bowen, J. P. & Hinchey, M. G. (Eds.) (1995). ZUM’95: The Z Formal Specification Notation. Lecture Notes in Computer Science: Vol. 967. Limerick: Springer.

    MATH  Google Scholar 

  14. Bowen, J. P., Hinchey, M. G., & Till, D. (Eds.) (1997). ZUM’97: The Z Formal Specification Notation. Lecture Notes in Computer Science: Vol. 1212. Berlin: Springer.

    Google Scholar 

  15. Bowen, J. P. & Nicholls, J. E. (Eds.) (1992). Seventh Annual Z User Workshop. London: Springer.

    Google Scholar 

  16. de Moura, L., Owre, S., Rueß, H., Rushby, J., Shankar, N., Sorea, M., & Tiwari, A. (2004). SAL 2. In R. Alur & D. Peled (Eds.), International Conference on Computer Aided Verification (CAV 2004). Lecture Notes in Computer Science: Vol. 3114 (pp. 496–500). Berlin: Springer.

    Chapter  Google Scholar 

  17. Davies, J. & Gibbons, J. (Eds.) (2007). Integrated Formal Methods, 6th International Conference, IFM 2007. Lecture Notes in Computer Science: Vol. 4591. Berlin: Springer.

    MATH  Google Scholar 

  18. Derrick, J., Fitzgerald, J. A., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., & Riccobene, E. (Eds.) (2012). Abstract State Machines, Alloy, B, VDM, and Z—Third International Conference, ABZ 2012. Lecture Notes in Computer Science: Vol. 7316. Berlin: Springer.

    MATH  Google Scholar 

  19. Derrick, J., North, S., & Simons, A. J. H. (2006). Issues in implementing a model checker for Z. In Z. Liu & J. He (Eds.), ICFEM. Lecture Notes in Computer Science: Vol. 4260 (pp. 678–696). Berlin: Springer.

    Google Scholar 

  20. Derrick, J., North, S., & Simons, A. J. H. (2008) Z2SAL—building a model checker for Z. In Börger et al. [7] (pp. 280–293).

    Google Scholar 

  21. Derrick, J., Boiten, E. A., & Reeves, S. (Eds.) (2011). Proceedings of the 15th International Refinement Workshop. Electronic Proceedings in Theoretical Computer Science: Vol. 55. Open Publishing Association.

    Google Scholar 

  22. Derrick, J., North, S., & Simons, A. J. H. (2011) Building a refinement checker for Z. In Derrick et al. [21] (pp. 37–52).

    Google Scholar 

  23. Derrick, J., North, S. D., & Simons, A. J. H. (2011). Z2SAL: a translation-based model checker for Z. Formal Aspects of Computing, 23(1), 43–71.

    Article  MATH  Google Scholar 

  24. Derrick, J., & Smith, G. (2008). Using model checking to automatically find retrieve relations. Electronic Notes in Theoretical Computer Science, 201, 155–175.

    Article  Google Scholar 

  25. Fitzgerald, J. A., Jones, C. B., & Lucas, P. (Eds.) (1997). FME’97: Industrial Application and Strengthened Foundations of Formal Methods. Lecture Notes in Computer Science: Vol. 1313. Berlin: Springer.

    Google Scholar 

  26. Frappier, M., Glässer, U., Khurshid, S., Laleau, R., & Reeves, S. (Eds.) (2010). ABZ 2010. Lecture Notes in Computer Science: Vol. 5977. Berlin: Springer.

    MATH  Google Scholar 

  27. Grimm, K. (1998) Industrial requirements for the efficient development of reliable embedded systems. In Bowen et al. [11] (pp. 1–4).

    Google Scholar 

  28. Hayes, I. J. (Ed.) (1987). Specification Case Studies. International Series in Computer Science. New York: Prentice Hall. 2nd ed., 1993.

    Google Scholar 

  29. Henson, M. C. (1998). The standard logic of Z is inconsistent. Formal Aspects of Computing, 10(3), 243–247.

    Article  MATH  Google Scholar 

  30. Henson, M. C., Deutsch, M., & Kajtazi, B. (2006). The specification logic nuZ. Formal Aspects of Computing, 18(3), 364–395.

    Article  MATH  Google Scholar 

  31. Henson, M. C., & Reeves, S. (1999). Revising Z: Part I—Logic and semantics. Formal Aspects of Computing, 11(4), 359–380.

    Article  MATH  Google Scholar 

  32. Henson, M. C., & Reeves, S. (1999). Revising Z: Part II—Logical development. Formal Aspects of Computing, 11(4), 381–401.

    Article  MATH  Google Scholar 

  33. Hinchey, M. G., & Bowen, J. P. (1995). Applications of Formal Methods. International Series in Computer Science. New York: Prentice Hall.

    MATH  Google Scholar 

  34. ISO/IEC (1999). Z notation: final committee draft. International Standard CD 13568.2. International Standards Organization.

    Google Scholar 

  35. ISO/IEC (2002). Information Technology—Z Formal Specification Notation—Syntax, Type System and Semantics. International Standard 13568, International Standards Organization. http://standards.iso.org/ittf/PubliclyAvailableStandards/c021573_ISO_IEC_13568_2002(E).zip.

  36. Jacky, J. (1997). The Way of Z: Practical Programming with Formal Methods. Cambridge: Cambridge University Press.

    Google Scholar 

  37. Jacky, J., Unger, J., Patrick, M., Reid, R., & Risler, R. (1997) Experience with Z developing a control program for a radiation therapy machine. In Bowen et al. [14] (pp. 317–328).

    Google Scholar 

  38. King, S. (1999). ‘The standard logic for Z’: a clarification. Formal Aspects of Computing, 11(4), 472–473.

    Article  MATH  Google Scholar 

  39. King, S., Hammond, J., Chapman, R., & Prior, A. (1999) The value of verification: positive experience of industrial proof. In Wing et al. [56] (pp. 1527–1545).

    Google Scholar 

  40. Leuschel, M., & Butler, M. (2003) ProB: A model checker for B. In Araki et al. [1] (pp. 855–874).

    Google Scholar 

  41. Leuschel, M., & Butler, M. (2005). Automatic refinement checking for B. In K. Lau & R. Banach (Eds.), International Conference on Formal Engineering Methods, ICFEM 2005. Lecture Notes in Computer Science: Vol. 3785 (pp. 345–359). Berlin: Springer.

    Google Scholar 

  42. Leuschel, M., & Massart, T. (2010). Efficient approximate verification of B and Z models via symmetry markers. Annals of Mathematics and Artificial Intelligence, 59(1), 81–106.

    Article  MathSciNet  MATH  Google Scholar 

  43. Nicholls, J. E. (Ed.) (1990). Z User Workshop, Oxford. Workshops in Computing. Berlin: Springer.

    Google Scholar 

  44. Plagge, D., & Leuschel, M. (2007) Validating Z specifications using the ProB animator and model checker. In Davies and Gibbons [17] (pp. 480–500).

    Google Scholar 

  45. Plagge, D., & Leuschel, M. (2010). Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more. International Journal on Software Tools for Technology Transfer, 12(1), 9–21.

    Article  Google Scholar 

  46. Potter, B., Sinclair, J., & Till, D. (1991). An Introduction to Formal Specification and Z. International Series in Computer Science. New York: Prentice Hall. 2nd ed., 1996.

    MATH  Google Scholar 

  47. Ratcliff, B. (1994). Introducing Specification Using Z: A Practical Case Study Approach. New York: McGraw-Hill.

    Google Scholar 

  48. Smith, G., & Derrick, J. (2005). Model checking downward simulations. Electronic Notes in Theoretical Computer Science, 137(2), 205–224.

    Article  Google Scholar 

  49. Smith, G., & Derrick, J. (2006). Verifying data refinements using a model checker. Formal Aspects of Computing, 18(3), 264–287.

    Article  MathSciNet  MATH  Google Scholar 

  50. Spivey, J. M. (1988). Understanding Z: A Specification Language and Its Formal Semantics. Cambridge: Cambridge University Press.

    MATH  Google Scholar 

  51. Spivey, J. M. (1989). The Z Notation: A Reference Manual. International Series in Computer Science. New York: Prentice Hall.

    MATH  Google Scholar 

  52. Spivey, J. M. (1992). The Z Notation: A Reference Manual (2nd ed.). International Series in Computer Science. New York: Prentice Hall.

    Google Scholar 

  53. Stringer-Calvert, D. W. J., Stepney, S., & Wand, I. (1997) Using PVS to prove a Z refinement: a case study. In Fitzgerald et al. [25] (pp. 573–588).

    Google Scholar 

  54. Toyn, I. (1998) Innovations in standard Z notation. In Bowen et al. [11] (pp. 193–213).

    Google Scholar 

  55. Treharne, H., King, S., Henson, M. C., & Schneider, S. A. (Eds.) (2005). ZB 2005: Formal Specification and Development in Z and B, 4th International Conference of B and Z Users. Lecture Notes in Computer Science: Vol. 3455. Berlin: Springer.

    Google Scholar 

  56. Wing, J. M., Woodcock, J. C. P., & Davies, J. (Eds.) (1999). FM’99 World Congress on Formal Methods in the Development of Computing Systems. Lecture Notes in Computer Science: Vol. 1708. Berlin: Springer.

    MATH  Google Scholar 

  57. Woodcock, J. C. P., & Davies, J. (1996). Using Z: Specification, Refinement, and Proof. New York: Prentice Hall.

    MATH  Google Scholar 

  58. Woodcock, J. C. P., Stepney, S., Cooper, D., Clark, J. A., & Jacob, J. (2008). The certification of the Mondex electronic purse to ITSEC Level E6. Formal Aspects of Computing, 20(1), 5–19.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Sheffield, Sheffield, UK

    John Derrick

  2. School of Computing, University of Kent, Canterbury, UK

    Eerke A. Boiten

Authors
  1. John Derrick
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Eerke A. Boiten
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer-Verlag London

About this chapter

Cite this chapter

Derrick, J., Boiten, E.A. (2014). An Introduction to Z. In: Refinement in Z and Object-Z. Springer, London. https://doi.org/10.1007/978-1-4471-5355-9_1

Download citation

  • DOI: https://doi.org/10.1007/978-1-4471-5355-9_1

  • Publisher Name: Springer, London

  • Print ISBN: 978-1-4471-5354-2

  • Online ISBN: 978-1-4471-5355-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation