Abstract
Consistency is essential for a Z specification to have any useful meaning. We give some sufficient conditions and stylistic guidelines for achieving it and for proving that this has been done. We also describe the Z interpretation of “undefined” expressions, and relate this to rules of proof. The paper is mainly tutorial; experience has shown that these issues have caused confusion.
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
Arthan, R.D.: On free type definitions in Z. In: Nicholls, J.E. (ed.) Z User Workshop in Computing, pp. 40–58. Springer, Heidelberg (1992)
Enderton, H.B.: Elements of Set Theory. Academic Press, London (1977)
Hall, J.G., Martin, A.P.: Wreconstructed. In: Till, D., Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 115–134. Springer, Heidelberg (1997)
Harwood, W.T.: Proof rules for Balzac. Technical Report WTH/P7/001, Imperial Software Technology, UK (1991)
Hall, J.G., McDermidan., J.A., Toyn, I.: Model conjectures for Z specifications. In: Habrias, H. (ed.) Z Twenty Years On – What is its Future?, IRIN, Université de Nantes, France, October 1995, pp. 41–51 (1995)
Jeffreys, S.H.: Scientific Inference, 2nd edn. Cambridge University Press, Cambridge (1957)
Jones, C.B.: Systematic Software Development using VDM. Prentice Hall Internationa Series in Computer Science (1986)
Saaltink, M.: Z and Eves. In: Nicholls, J.E. (ed.) Z User Workshop, York. Workshops in Computing, pp. 223–242. Springer, Heidelberg (1992)
Smith, A.: On recursive free types in Z. In: Nicholls, J.E. (ed.) Z User Workshop in Computing 1991, pp. 3–39. Springer, Heidelberg (1992)
Spivey, J.M.: Understanding Z. Cambridge University Press, Cambridge (1988)
Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice Hall, Englewood Cliffs (1992)
Toyn, I.: CADiZWeb pages (1998), http://www.cs.york.ac.uk/~ian/cadiz/
Toyn, I.: Innovations in standard Z. In: Bowen, J.P., Fett, A., Hinchey, M.G. (eds.) ZUM 1998. LNCS, vol. 1493, pp. 193–214. Springer, Heidelberg (1998)
Toyn, I. (ed.): Z Notation. ISO (1998) (to appear)
Woodcock, J.C.P., Davies, J.: Using Z – Specification, Refinement and Proof. Prentice Hall International Series in Computer Science (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Valentine, S.H. (1998). Inconsistency and Undefinedness in Z – A Practical Guide. In: Bowen, J.P., Fett, A., Hinchey, M.G. (eds) ZUM ’98: The Z Formal Specification Notation. ZUM 1998. Lecture Notes in Computer Science, vol 1493. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-49676-2_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-49676-2_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65070-6
Online ISBN: 978-3-540-49676-2
eBook Packages: Springer Book Archive