An Object-Oriented Structuring for Z Based on Views

  • Nuno Amálio
  • Fiona Polack
  • Susan Stepney
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3455)


There is significant interest in the use of Z in conjunction with object-orientation. Here we present a new approach to structuring Z specifications in an object-oriented (OO) style. Our structuring is based on views, it uses the schema calculus, and it does not extend Z. The resulting OO Z specifications are comprehensible, modular, and conceptually clear. The modularity of the new approach supports a template-instantiation approach to expressing OO models in Z; practical formal verification and validation of the model can be undertaken using meta-proof, meta-lemmas, and formal snapshots.




Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Stepney, S., Barden, R., Cooper, D. (eds.): Object orientation in Z. In: Workshops in Computing. Springer, Heidelberg (1992)Google Scholar
  2. 2.
    Smith, G.P.: The Object-Z Specification Language. Kluwer Academic Publishers, Dordrecht (2000)zbMATHGoogle Scholar
  3. 3.
    Amálio, N., Stepney, S., Polack, F.: Modular UML semantics: Interpretations in Z based on templates and generics. In: Van, H.D., Liu, Z. (eds.) FACS 2003. UNU/IIST Technical Report, vol. 284, pp. 81–100 (2003)Google Scholar
  4. 4.
    Amálio, N., Stepney, S., Polack, F.: Formal proof from UML models. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 418–433. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  5. 5.
    Amálio, N., Polack, F., Stepney, S.: A modelling and analysis framework for sequential systems I: Modelling. Technical Report YCS-2005, Department of Computer Science, University of York (2005)Google Scholar
  6. 6.
    Amálio, N., Polack, F.: Comparison of formalisation approaches of UML class constructs in Z and Object-Z. In: Bert, et al. [18], pp. 339–358Google Scholar
  7. 7.
    Jackson, D.: Structuring Z specifications with views. ACM Transactions on Software Engineering and Methodology 4(4), 365–389 (1995)CrossRefGoogle Scholar
  8. 8.
    Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)Google Scholar
  9. 9.
    Stepney, S., Polack, F., Toyn, I.: Patterns to guide practical refactoring: examples targetting promotion in Z. In: Bert, et al.[18], pp. 20–39Google Scholar
  10. 10.
    Amálio, N., Stepney, S., Polack, F.: Modular meta-proof for structured specifications (2004) Available at,
  11. 11.
    Stepney, S., Polack, F., Toyn, I.: A Z patterns catalogue I, specification and refactoring. Technical Report YCS-2003-349, Department of Computer Science, University of York (2003)Google Scholar
  12. 12.
    Barden, R., Stepney, S., Cooper, D.: Z In Practice. Practitioner Series. Prentice–Hall, Englewood Cliffs (1994)zbMATHGoogle Scholar
  13. 13.
    Borgida, A., Mylopoulos, J., Reiter, R.: On the frame problem in procedure specifications. IEEE Transactions on Software Engineering 21(10), 785–798 (1995)CrossRefGoogle Scholar
  14. 14.
    Hall, A.: Using Z as a specification calculus for object-oriented systems. In: Langmaack, H., Hoare, C.A.R., Bjorner, D. (eds.) VDM 1990. LNCS, vol. 428, pp. 290–318. Springer, Heidelberg (1990)Google Scholar
  15. 15.
    Hall, A.: Specifying and interpreting class hierarchies in Z. In: Bowen, J., Hall, A. (eds.) Workshops in Computing,Z User Workshop, pp. 120–138. Springer, Heidelberg (1994)Google Scholar
  16. 16.
    Utting, M., Wang, S.: Object orientation without extending Z. In: Bert et al.[18], pp. 319–338Google Scholar
  17. 17.
    Jackson, D., Shlyakhter, I., Sridharan, M.: A micromodularity mechanism. In: ACM SIGSOFT Foundation of Software Engineering/ Europoean Software Engineering Conference (2001)Google Scholar
  18. 18.
    Bert, D., et al. (eds.): ZB 2003. LNCS, vol. 2651. Springer, Heidelberg (2003)zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Nuno Amálio
    • 1
  • Fiona Polack
    • 1
  • Susan Stepney
    • 1
  1. 1.Department of Computer ScienceUniversity of YorkYorkUK

Personalised recommendations