Abstract
It is well known that the principal operators in the Z schema calculus are not monotonic with respect to either operation or data refinement. This is generally regarded as limiting their usefulness in software development, and has lead to proposals to redefine the schema calculus and/or the notion of refinement so that monotonicity is established. We examine this issue more closely, to demonstrate just how non-monotonicity arises, and identify various conditions under which components of schema expressions can be safely replaced by their refinements. This shows that in a wide range of practical situations, refinement of such components can be justified by checking fairly simple conditions.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Spivey, M.: The Z Notation: A Reference Manual. Prentice-Hall International, Englewood Cliffs (1988); 2nd edn. (1992)
Woodcock, J., Davies, J.: Using Z: Specification, Refinement and Proof. Prentice-Hall International, Englewood Cliffs (1996)
Derrick, J., Boiten, E.: Refinement in Z and Object-Z: Foundations and Advanced Applications. Springer, Heidelberg (2001)
Henson, M.C., Reeves, S.: Program development and specification refinement in the schema calculus. In: Bowen, J.P., Dunne, S., Galloway, A., King, S. (eds.) B 2000, ZUM 2000, and ZB 2000. LNCS, vol. 1878, pp. 344–362. Springer, Heidelberg (2000)
Groves, L.: Refinement and the Z schema calculus. In: Woodcock, J., Derrick, J., Boiten, E., von Wright, J. (eds.) Proc. REFINE 2002, Copenhagen, July 20-21, 2002. Electronic Notes in Theoretical Computer Science, vol. 70(3) (2002), http://www.mcs.vuw.ac.nz/~lindsay/Papers
Barden, R., Stepney, S., Cooper, D.: The use of Z. In: Nicholls, J.E. (ed.) Proc. 6th Z User Meeting, York 1991, Workshops in Computing, pp. 99–124. Springer, Heidelberg (1992)
Hayes, I.: Specification Case Studies, 2nd edn. Prentice-Hall, Englewood Cliffs (1993)
Morgan, C.: Programming from Specifications, 2nd edn. Prentice Hall, Englewood Cliffs (1994)
Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer, Heidelberg (1998)
Wordsworth, J.: Software Development with Z. Addison-Wesley, Reading (1992)
Woodcock, J.C.P.: Implementing promoted operations in Z. In: Jones, C.B., Shaw, R.C., Denvir, T. (eds.) Proceedings of the 5th BCS Refinement Workshop, pp. 367–378. Springer, Heidelberg (1992)
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
Groves, L. (2005). Practical Data Refinement for the Z Schema Calculus. 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_23
Download citation
DOI: https://doi.org/10.1007/11415787_23
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)