{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,3]],"date-time":"2026-06-03T15:45:27Z","timestamp":1780501527118,"version":"3.54.1"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319296272","type":"print"},{"value":"9783319296289","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-29628-9_3","type":"book-chapter","created":{"date-parts":[[2016,2,28]],"date-time":"2016-02-28T21:04:31Z","timestamp":1456693471000},"page":"103-151","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["The Z Notation: Whence the Cause and Whither the Course?"],"prefix":"10.1007","author":[{"given":"Jonathan P.","family":"Bowen","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,3,1]]},"reference":[{"key":"3_CR1","unstructured":"Abrial, J.R.: Data semantics. In: Klimbie, J.W., Koffeman, K.L. (eds.) IFIP TC2 Working Conference on Data Base Management, pp. 1\u201359. Elsevier Science Publishers, North-Holland, April 1974"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-319-15201-1_3","volume-title":"Software Engineering and Formal Methods","author":"SM Bagheri","year":"2015","unstructured":"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\u201353. Springer, Heidelberg (2015)"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Boulanger, J.L. (ed.): Formal Methods: Industrial Use from Model to the Code. ISTE, Wiley, London (2012)","DOI":"10.1002\/9781118561829"},{"issue":"1\u20135","key":"3_CR4","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0165-6074(87)90042-1","volume":"21","author":"JP Bowen","year":"1987","unstructured":"Bowen, J.P.: Formal specification and documentation of microprocessor instruction sets. Microprocessing and Microprogramming 21(1\u20135), 223\u2013230 (1987)","journal-title":"Microprocessing and Microprogramming"},{"key":"3_CR5","unstructured":"Bowen, J.P. (ed.): Proceeding of Z Users Meeting, 1 Wellington Square, Oxford. Oxford University Computing Laboratory, Oxford, December 1987"},{"key":"3_CR6","unstructured":"Bowen, J.P.: Formal specification in Z as a design and documentation tool. In: Proc. 2nd IEE\/BCS Conference on Software Engineering, pp. 164\u2013168, No. 290 in Conference Publication. IEE\/BCS, July 1988"},{"issue":"1","key":"3_CR7","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1049\/sej.1989.0008","volume":"4","author":"JP Bowen","year":"1989","unstructured":"Bowen, J.P.: POS: formal specification of a UNIX tool. IEE\/BCS Softw. Eng. J. 4(1), 67\u201372 (1989)","journal-title":"IEE\/BCS Softw. Eng. J."},{"issue":"4","key":"3_CR8","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1111\/1467-8659.1140221","volume":"11","author":"JP Bowen","year":"1992","unstructured":"Bowen, J.P.: X: why Z? Comput. Graph. Forum 11(4), 221\u2013234 (1992)","journal-title":"Comput. Graph. Forum"},{"issue":"5\u20136","key":"3_CR9","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0950-5849(95)90001-2","volume":"37","author":"JP Bowen","year":"1995","unstructured":"Bowen, J.P.: Glossary of Z notation. Inf. Softw. Technol. 37(5\u20136), 333\u2013334 (1995)","journal-title":"Inf. Softw. Technol."},{"key":"3_CR10","volume-title":"Formal Specification and Documentation Using Z: A Case Study Approach","author":"JP Bowen","year":"1996","unstructured":"Bowen, J.P.: Formal Specification and Documentation Using Z: A Case Study Approach. International Thomson Computer Press, London (1996)"},{"issue":"2","key":"3_CR11","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/505776.505794","volume":"26","author":"JP Bowen","year":"2001","unstructured":"Bowen, J.P.: Experience teaching Z with tool and web support. ACM SIGSOFT Softw. Eng. Notes 26(2), 69\u201375 (2001)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"3_CR12","unstructured":"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\u201320. ISTE (2006)"},{"key":"3_CR13","first-page":"270","volume-title":"The Scientists: An Epic of Discovery","author":"JP Bowen","year":"2012","unstructured":"Bowen, J.P.: Alan Turing. In: Robinson, A. (ed.) The Scientists: An Epic of Discovery, pp. 270\u2013275. Thames and Hudson, London (2012)"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","first-page":"24","volume-title":"ZUM\u201998: The Z Formal Specification Notation","year":"1998","unstructured":"Bowen, J.P., Fett, A., Hinchey, M.G. (eds.): ZUM\u201998: The Z Formal Specification Notation. LNCS, vol. 1493, pp. 24\u201326. Springer, Heidelberg (1998)"},{"key":"3_CR15","unstructured":"Bowen, J.P., Gimson, R.B., Topp-J\u00f8rgensen, S.: Specifying system implementations in Z. Technical Monograph PRG-63, Oxford University Computing Laboratory, Oxford, February 1988"},{"issue":"5\u20136","key":"3_CR16","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0950-5849(95)99362-Q","volume":"37","author":"JP Bowen","year":"1995","unstructured":"Bowen, J.P., Gordon, M.J.C.: A shallow embedding of Z in HOL. Inf. Softw. Technol. 37(5\u20136), 269\u2013276 (1995)","journal-title":"Inf. Softw. Technol."},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-642-11447-2_14","volume-title":"Rigorous Methods for Software Construction and Analysis","author":"JP Bowen","year":"2009","unstructured":"Bowen, J.P., Hinchey, M.G.: Ten commandments ten years on: lessons for ASM, B, Z and VSR-net. In: Abrial, J.-R., Gl\u00e4sser, U. (eds.) Rigorous Methods for Software Construction and Analysis. LNCS, vol. 5115, pp. 219\u2013233. Springer, Heidelberg (2009)"},{"key":"3_CR18","unstructured":"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\u201325. CRC Press (2014)"},{"issue":"10","key":"3_CR19","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1109\/MC.2014.284","volume":"47","author":"JP Bowen","year":"2014","unstructured":"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\u201389 (2014)","journal-title":"IEEE Comput."},{"key":"3_CR20","series-title":"Workshops in Computing","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/978-1-4471-3452-7_11","volume-title":"Z User Workshop, Cambridge 1994","author":"PT Breuer","year":"1994","unstructured":"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\u2013209. Springer, London (1994)"},{"key":"3_CR21","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1023\/A:1018965316985","volume":"3","author":"P Ciancarini","year":"1997","unstructured":"Ciancarini, P., Cimato, S., Mascolo, C.: Engineering formal requirements: an analysis and testing method for Z documents. Ann. Softw. Eng. 3, 189\u2013219 (1997)","journal-title":"Ann. Softw. Eng."},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Copeland, J., Bowen, J.P., Sprevak, M., Wilson, R.J., et al.: The Turing Guide. Oxford University Press (to appear 2016)","DOI":"10.1093\/oso\/9780198747826.001.0001"},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"601","DOI":"10.1007\/978-3-642-24559-6_40","volume-title":"Formal Methods and Software Engineering","author":"M Cristia","year":"2011","unstructured":"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\u2013616. Springer, Heidelberg (2011)"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Gimson, R., Bowen, J.P., Gleeson, T.: Distributed computing software project. In: 2nd Workshop on Making Distributed Systems Work, pp. 1\u20133. ACM, September 1986","DOI":"10.1145\/503956.503978"},{"key":"3_CR25","doi-asserted-by":"publisher","DOI":"10.1002\/9781118459898","volume-title":"Formal Methods for Industrial Critical Systems: A Survey of Applications","author":"S Gnesi","year":"2012","unstructured":"Gnesi, S., Margaria, T.: Formal Methods for Industrial Critical Systems: A Survey of Applications. IEEE Computer Society Press, Wiley, Chichester (2012)"},{"key":"3_CR26","unstructured":"Hall, J.A.: Z word tools. SourceForge (2008). http:\/\/sourceforge.net\/projects\/zwordtools\/. Accessed 28 September 2015"},{"issue":"4","key":"3_CR27","first-page":"381","volume":"22","author":"MC Henson","year":"2003","unstructured":"Henson, M.C., Reeves, S., Bowen, J.P.: Z logic and its consequences. CAI. Comput. Inform. 22(4), 381\u2013415 (2003)","journal-title":"CAI. Comput. Inform."},{"issue":"9","key":"3_CR28","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1145\/1378727.1378742","volume":"51","author":"MG Hinchey","year":"2008","unstructured":"Hinchey, M.G., Jackson, M., Cousot, P., Cook, B., Bowen, J.P., Margaria, T.: Software engineering and formal methods. Commun. ACM 51(9), 54\u201359 (2008)","journal-title":"Commun. ACM"},{"issue":"10","key":"3_CR29","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"3_CR30","series-title":"Series in Computer Science","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Series in Computer Science. Prentice Hall International, London (1985)"},{"key":"3_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/3-540-60271-2_118","volume-title":"ZUM\u201995: The Z Formal Specification Notation","author":"HM H\u00f6rcher","year":"1995","unstructured":"H\u00f6rcher, H.M.: Improving software tests using Z specifications. In: Bowen, J.P., Hinchey, M.G. (eds.) ZUM\u201995: The Z Formal Specification Notation. LNCS, vol. 967, pp. 152\u2013166. Springer, Heidelberg (1995)"},{"key":"3_CR32","unstructured":"ISO: Information technology - Z formal specification notation - syntax, type system and semantics. International Standard 13568, ISO\/IEC, July 2002"},{"issue":"1","key":"3_CR33","first-page":"10","volume":"1","author":"RB Jones","year":"1992","unstructured":"Jones, R.B.: ICL ProofPower. BCS-FACS FACTS Series III 1(1), 10\u201313 (1992)","journal-title":"BCS-FACS FACTS Series III"},{"issue":"2","key":"3_CR34","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1109\/MAHC.1984.10017","volume":"6","author":"FL Morris","year":"1984","unstructured":"Morris, F.L., Jones, C.B.: An early program proof by Alan Turing. IEEE Ann. Hist. Comput. 6(2), 139\u2013143 (1984)","journal-title":"IEEE Ann. Hist. Comput."},{"key":"3_CR35","series-title":"Workshops in Computing","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-1-4471-3540-1_22","volume-title":"Z User Workshop, Oxford 1990","author":"JE Nicholls","year":"1991","unstructured":"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\u2013350. Springer, Heidelberg (1991)"},{"key":"3_CR36","series-title":"Workshops in Computing","volume-title":"Z User Workshop, York 1991","year":"1992","unstructured":"Nicholls, J.E. (ed.): Z User Workshop, York 1991. Workshops in Computing. Springer, London (1992)"},{"key":"3_CR37","series-title":"Lecture Notes in Computer Science","volume-title":"ZUM\u201997: The Z Formal Specification Notation","author":"M Saaltink","year":"1997","unstructured":"Saaltink, M.: The Z\/EVES system. In: Till, D., Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol. 1212. Springer, Heidelberg (1997)"},{"key":"3_CR38","unstructured":"Smith, G.: The Object-Z Specification Language, Advances in Formal Methods, vol. 1. Springer, Heidelberg (2012)"},{"key":"3_CR39","unstructured":"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\/"},{"key":"3_CR40","unstructured":"Spivey, J.M.: The fuzz type-checker for Z. Technical report, University of Oxford, UK (2008). http:\/\/spivey.oriel.ox.ac.uk\/mike\/fuzz\/"},{"issue":"11","key":"3_CR41","doi-asserted-by":"publisher","first-page":"777","DOI":"10.1109\/32.553698","volume":"22","author":"P Stocks","year":"1996","unstructured":"Stocks, P., Carrington, D.: A framework for specification-based testing. IEEE Trans. Softw. Eng. 22(11), 777\u2013793 (1996)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"1","key":"3_CR42","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1112\/plms\/s2-42.1.230","volume":"s2-42","author":"A. M. Turing","year":"1937","unstructured":"Turing, A.M.: On computable numbers with an application to the Entscheidungsproblem. Proc. London Math. Soc. 2(42), 230\u2013265 (1936\/7)","journal-title":"Proceedings of the London Mathematical Society"},{"key":"3_CR43","unstructured":"Turing, A.M.: Checking a large routine. In: Campbell-Kelly, M. (ed.) The early British computer conferences, pp. 70\u201372. MIT Press, Cambridge (1949\/1989)"},{"key":"3_CR44","doi-asserted-by":"crossref","unstructured":"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\u2013356. IEEE Computer Society Press, 8\u201312 October 2001","DOI":"10.1109\/CMPSAC.2001.960638"},{"issue":"1","key":"3_CR45","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/s00165-005-0084-7","volume":"18","author":"SA Vilkomir","year":"2006","unstructured":"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\u201362 (2006)","journal-title":"Formal Aspects Comput."}],"container-title":["Lecture Notes in Computer Science","Engineering Trustworthy Software Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-29628-9_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T09:57:52Z","timestamp":1770371872000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-29628-9_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319296272","9783319296289"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29628-9_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"1 March 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}