Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Stepney, S., Barden, R., Cooper, D. (eds.): Object orientation in Z. In: Workshops in Computing. Springer, Heidelberg (1992)
Smith, G.P.: The Object-Z Specification Language. Kluwer Academic Publishers, Dordrecht (2000)
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)
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)
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)
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–358
Jackson, D.: Structuring Z specifications with views. ACM Transactions on Software Engineering and Methodology 4(4), 365–389 (1995)
Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)
Stepney, S., Polack, F., Toyn, I.: Patterns to guide practical refactoring: examples targetting promotion in Z. In: Bert, et al.[18], pp. 20–39
Amálio, N., Stepney, S., Polack, F.: Modular meta-proof for structured specifications (2004) Available at, http://www.cs.york.ac.uk/~namalio/publications.html
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)
Barden, R., Stepney, S., Cooper, D.: Z In Practice. Practitioner Series. Prentice–Hall, Englewood Cliffs (1994)
Borgida, A., Mylopoulos, J., Reiter, R.: On the frame problem in procedure specifications. IEEE Transactions on Software Engineering 21(10), 785–798 (1995)
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)
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)
Utting, M., Wang, S.: Object orientation without extending Z. In: Bert et al.[18], pp. 319–338
Jackson, D., Shlyakhter, I., Sridharan, M.: A micromodularity mechanism. In: ACM SIGSOFT Foundation of Software Engineering/ Europoean Software Engineering Conference (2001)
Bert, D., et al. (eds.): ZB 2003. LNCS, vol. 2651. Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Amálio, N., Polack, F., Stepney, S. (2005). An Object-Oriented Structuring for Z Based on Views. In: Treharne, H., King, S., Henson, M., Schneider, S. (eds) ZB 2005: Formal Specification and Development in Z and B. ZB 2005. Lecture Notes in Computer Science, vol 3455. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11415787_16
Download citation
DOI: https://doi.org/10.1007/11415787_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25559-8
Online ISBN: 978-3-540-32007-4
eBook Packages: Computer ScienceComputer Science (R0)