Engineering Trustworthy Software Systems pp 103-151 | Cite as

# The Z Notation: Whence the Cause and Whither the Course?

## Abstract

The Z notation for the formal specification of computer-based systems has been in existence since the early 1980s. Since then, an international Z community has emerged, academic and industrial courses have been developed, an ISO standard has been adopted, and Z has been used on a number of significant software development projects, especially where safety and security have been important. This chapter traces the history of the Z notation and presents issues in teaching Z, with examples. A specific example of an industrial course is presented. Although subsequent notations have been developed, with better tool support, Z is still an excellent choice for general purpose specification and is especially useful in directing software testing to ensure good coverage.

## Keywords

State Component State Schema Operation Schema Predicate Part Program Research Group## Notes

### Acknowledgements

Material for the Z course was kindly made available by Altran UK (formerly Altran Praxis), a software engineering company based in the United Kingdom with extensive experience of the industrial use of formal methods in general and the Z notation in particular. The extracts of the Z course included in Appendix B are copyright Altran UK and are reproduced here with permission. I am very grateful to Jonathan Hammond of Altran UK for his help and advice in this matter. Thomas Lancaster of Birmingham City University invited me to contribution to a Z course for final year undergraduates. The questions and answers on an example air traffic control system as presented here were originally developed as a result.

The Z notation in the main part of this chapter has been formatted using the Open image in new window style file zed-csp.sty and type-checked using the Open image in new window type-checker [40]. It is believed that the drawing in Fig. 2 is by Ib Holm Sørensen (who died in 2012), from an idea by Bernard Sufrin.

Many thanks to my good colleague, Prof. Zhiming Liu, for inviting me to present at the Summer School on Engineering Trustworthy Software Systems (SETSS) at Southwest University in Chongqing, China, during September 2014, and thank you to all at Southwest University for a very pleasant and well organized visit, together with financial support. I am grateful too for financial support from Museophile Limited.

Finally, very many thanks to the Israel Institute for Advanced Studies at the Hebrew University of Jerusalem, who funded me as a Visiting Scholar for a Computability Research Group during the completion of this chapter and provided a very supportive academic environment in which to do it.

## Supplementary material

## References

- 1.Abrial, J.R.: Data semantics. In: Klimbie, J.W., Koffeman, K.L. (eds.) IFIP TC2 Working Conference on Data Base Management, pp. 1–59. Elsevier Science Publishers, North-Holland, April 1974Google Scholar
- 2.Bagheri, S.M., Smith, G., Hanan, J.: Using Z in the development and maintenance of computational models of real-world systems. In: Canal, C., Idani, A. (eds.) SEFM 2014 Workshops. LNCS, vol. 8938, pp. 36–53. Springer, Heidelberg (2015)Google Scholar
- 3.Boulanger, J.L. (ed.): Formal Methods: Industrial Use from Model to the Code. ISTE, Wiley, London (2012)Google Scholar
- 4.Bowen, J.P.: Formal specification and documentation of microprocessor instruction sets. Microprocessing and Microprogramming
**21**(1–5), 223–230 (1987)CrossRefGoogle Scholar - 5.Bowen, J.P. (ed.): Proceeding of Z Users Meeting, 1 Wellington Square, Oxford. Oxford University Computing Laboratory, Oxford, December 1987Google Scholar
- 6.Bowen, J.P.: Formal specification in Z as a design and documentation tool. In: Proc. 2nd IEE/BCS Conference on Software Engineering, pp. 164–168, No. 290 in Conference Publication. IEE/BCS, July 1988Google Scholar
- 7.Bowen, J.P.: POS: formal specification of a UNIX tool. IEE/BCS Softw. Eng. J.
**4**(1), 67–72 (1989)MathSciNetCrossRefGoogle Scholar - 8.Bowen, J.P.: X: why Z? Comput. Graph. Forum
**11**(4), 221–234 (1992)MathSciNetCrossRefGoogle Scholar - 9.Bowen, J.P.: Glossary of Z notation. Inf. Softw. Technol.
**37**(5–6), 333–334 (1995)CrossRefGoogle Scholar - 10.Bowen, J.P.: Formal Specification and Documentation Using Z: A Case Study Approach. International Thomson Computer Press, London (1996)Google Scholar
- 11.Bowen, J.P.: Experience teaching Z with tool and web support. ACM SIGSOFT Softw. Eng. Notes
**26**(2), 69–75 (2001)CrossRefGoogle Scholar - 12.Bowen, J.P.: Z: A formal specification notation. In: Frappier, M., Habrias, H. (eds.) Software Specification Methods: An Overview Using a Case Study, chap. 1, pp. 3–20. ISTE (2006)Google Scholar
- 13.Bowen, J.P.: Alan Turing. In: Robinson, A. (ed.) The Scientists: An Epic of Discovery, pp. 270–275. Thames and Hudson, London (2012)Google Scholar
- 14.Bowen, J.P., Fett, A., Hinchey, M.G. (eds.): ZUM’98: The Z Formal Specification Notation. LNCS, vol. 1493, pp. 24–26. Springer, Heidelberg (1998)Google Scholar
- 15.Bowen, J.P., Gimson, R.B., Topp-Jørgensen, S.: Specifying system implementations in Z. Technical Monograph PRG-63, Oxford University Computing Laboratory, Oxford, February 1988Google Scholar
- 16.Bowen, J.P., Gordon, M.J.C.: A shallow embedding of Z in HOL. Inf. Softw. Technol.
**37**(5–6), 269–276 (1995)CrossRefGoogle Scholar - 17.Bowen, J.P., Hinchey, M.G.: Ten commandments ten years on: lessons for ASM, B, Z and VSR-net. In: Abrial, J.-R., Glässer, U. (eds.) Rigorous Methods for Software Construction and Analysis. LNCS, vol. 5115, pp. 219–233. Springer, Heidelberg (2009)CrossRefGoogle Scholar
- 18.Bowen, J.P., Hinchey, M.G.: Formal methods. In: Gonzalez, T.F., Diaz-Herrera, J., Tucker, A.B. (eds.) Computing Handbook, vol. 1, 3rd edn., chap. 71, pp. 1–25. CRC Press (2014)Google Scholar
- 19.Bowen, J.P., Hinchey, M.G., Janicke, H., Ward, M., Zedan, H.: Formality, agility, security, and evolution in software development. IEEE Comput.
**47**(10), 86–89 (2014)CrossRefGoogle Scholar - 20.Breuer, P.T., Bowen, J.P.: Towards correct executable semantics for Z. In: Bowen, J.P., Hall, J.A. (eds.) Z User Workshop, Cambridge 1994. Workshops in Computing, pp. 185–209. Springer, London (1994)CrossRefGoogle Scholar
- 21.Ciancarini, P., Cimato, S., Mascolo, C.: Engineering formal requirements: an analysis and testing method for Z documents. Ann. Softw. Eng.
**3**, 189–219 (1997)CrossRefGoogle Scholar - 22.Copeland, J., Bowen, J.P., Sprevak, M., Wilson, R.J., et al.: The Turing Guide. Oxford University Press (to appear 2016)Google Scholar
- 23.Cristia, M., Hollmann, D., Albertengo, P., Frydman, C., Monetti, P.R.: A language for test case refinement in the test template framework. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 601–616. Springer, Heidelberg (2011)CrossRefGoogle Scholar
- 24.Gimson, R., Bowen, J.P., Gleeson, T.: Distributed computing software project. In: 2nd Workshop on Making Distributed Systems Work, pp. 1–3. ACM, September 1986Google Scholar
- 25.Gnesi, S., Margaria, T.: Formal Methods for Industrial Critical Systems: A Survey of Applications. IEEE Computer Society Press, Wiley, Chichester (2012)CrossRefGoogle Scholar
- 26.Hall, J.A.: Z word tools. SourceForge (2008). http://sourceforge.net/projects/zwordtools/. Accessed 28 September 2015
- 27.Henson, M.C., Reeves, S., Bowen, J.P.: Z logic and its consequences. CAI. Comput. Inform.
**22**(4), 381–415 (2003)MathSciNetzbMATHGoogle Scholar - 28.Hinchey, M.G., Jackson, M., Cousot, P., Cook, B., Bowen, J.P., Margaria, T.: Software engineering and formal methods. Commun. ACM
**51**(9), 54–59 (2008)CrossRefGoogle Scholar - 29.Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM
**12**(10), 576–580 (1969)CrossRefzbMATHGoogle Scholar - 30.Hoare, C.A.R.: Communicating Sequential Processes. Series in Computer Science. Prentice Hall International, London (1985)zbMATHGoogle Scholar
- 31.Hörcher, H.M.: Improving software tests using Z specifications. In: Bowen, J.P., Hinchey, M.G. (eds.) ZUM’95: The Z Formal Specification Notation. LNCS, vol. 967, pp. 152–166. Springer, Heidelberg (1995)CrossRefGoogle Scholar
- 32.ISO: Information technology - Z formal specification notation - syntax, type system and semantics. International Standard 13568, ISO/IEC, July 2002Google Scholar
- 33.Jones, R.B.: ICL ProofPower. BCS-FACS FACTS Series III
**1**(1), 10–13 (1992)Google Scholar - 34.Morris, F.L., Jones, C.B.: An early program proof by Alan Turing. IEEE Ann. Hist. Comput.
**6**(2), 139–143 (1984)MathSciNetCrossRefzbMATHGoogle Scholar - 35.Nicholls, J.E.: A survey of Z courses in the UK. In: Nicholls, J.E. (ed.) Z User Workshop, Oxford 1990. Workshops in Computing, pp. 343–350. Springer, Heidelberg (1991)CrossRefGoogle Scholar
- 36.Nicholls, J.E. (ed.): Z User Workshop, York 1991. Workshops in Computing. Springer, London (1992)Google Scholar
- 37.Saaltink, M.: The Z/EVES system. In: Till, D., Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol. 1212. Springer, Heidelberg (1997)Google Scholar
- 38.Smith, G.: The Object-Z Specification Language, Advances in Formal Methods, vol. 1. Springer, Heidelberg (2012)Google Scholar
- 39.Spivey, J.M.: The Z Notation: A reference manual. Series in Computer Science, Prentice Hall International (1989/1992/2001). http://spivey.oriel.ox.ac.uk/mike/zrm/
- 40.Spivey, J.M.: The fuzz type-checker for Z. Technical report, University of Oxford, UK (2008). http://spivey.oriel.ox.ac.uk/mike/fuzz/
- 41.Stocks, P., Carrington, D.: A framework for specification-based testing. IEEE Trans. Softw. Eng.
**22**(11), 777–793 (1996)CrossRefGoogle Scholar - 42.Turing, A.M.: On computable numbers with an application to the Entscheidungsproblem. Proc. London Math. Soc.
**2**(42), 230–265 (1936/7)Google Scholar - 43.Turing, A.M.: Checking a large routine. In: Campbell-Kelly, M. (ed.) The early British computer conferences, pp. 70–72. MIT Press, Cambridge (1949/1989)Google Scholar
- 44.Vilkomir, S.A., Bowen, J.P.: Formalization of software testing criteria using the Z notation. In: Proceeding 25th Annual International Computer Software and Applications Conference (COMPSAC 2001), Chicago, pp. 351–356. IEEE Computer Society Press, 8–12 October 2001Google Scholar
- 45.Vilkomir, S.A., Bowen, J.P.: From MC/DC to RC/DC: formalization and analysis of control-flow testing criteria. Formal Aspects Comput.
**18**(1), 42–62 (2006)CrossRefzbMATHGoogle Scholar