Z swMATH ID: 10291 Software Authors: Woodcock, Jim; Davies, Jim Description: Using Z. Specification, refinement, and proof. The book is an in-depth introduction to the specification language \(Z\). It is primarily directed to the user; the background theory is – with the exception of the natural deduction calculus, see below – only introduction as far as necessary. With respect to the many \(Z\) books already on the market, a significant novel feature is the integration of \(Z\) with the refinement calculus and data refinement. The overall presentation is fluent, with many well-chosen examples. Throughout the authors strive to make reading as entertaining as possible. However, there are quite a number of minor unclarities, inconsistencies and errors (both in semantics and spelling). This gives the impression that the book was finished somewhat in a rush. What I find least satisfactory about the book is the broad and tedious exposition of the natural deduction calculus, which is not used further on in the book. Rather, most proofs are omitted and replaced by an appeal to the reader’s intuition. Is this adquate for promoting a discipline of formal specification and reasoning? Another disappointment is that in those places where proofs are given, the treatment often is quite cumbersome. In particular, although all necessary notions from the relational calculus are introduced, its algebraic properties are not mentioned; many of the proofs about relational notions could have been given much more simply and elegantly by relational algebra than in the pointwise fashion used in the book. Nevertheless I think the book is interesting and worthwhile reading for newcomers to \(Z\) with a certain amount of mathematical inclination. Homepage: http://en.wikipedia.org/wiki/Z_notation Keywords: data refinement; refinement calculus; specification language \(Z\) Related Software: Circus; ProofPower; Rodin; Z/EVES; Eiffel; Isabelle/HOL; PVS; SPIN; ProB; Haskell; Coq; HOL; JML; ZRC; FDR2; ML; Isabelle/UTP; Isabelle; KIV; Simulink Cited in: 228 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year The Z Notation. A Reference Manual. Zbl 0777.68003Spivey, J. M. 1989 all top 5 Cited by 351 Authors 25 Cavalcanti, Ana 21 Woodcock, James C. P. 11 Derrick, John 8 Zeyda, Frank 7 Boiten, Eerke A. 7 Smith, Graeme 6 Hayes, Ian J. 6 Schellhorn, Gerhard 6 Wehrheim, Heike 5 Colvin, Robert J. 5 Cristiá, Maximiliano 5 Freitas, Leo 5 Kahl, Wolfram 5 Rossi, Gianfranco 4 Banach, Richard 4 Bjørner, Dines 4 Foster, Simon 4 Martins Moreira, Anamaria 4 Oliveira, Marcel 4 Reeves, Steve 4 Sampaio, Augusto C. A. 4 Streader, David 3 Liu, Zhiming 3 Mota, Alexandre C. 3 Olderog, Ernst-Rüdiger 3 Ribeiro, Pedro 3 Wei, Kun 2 Barbosa, Luís Soares 2 Bowen, Jonathan P. 2 Burns, Alan D. 2 Chen, Yifeng 2 da Costa, Umberto Souza 2 Déharbe, David 2 Fu, Zheng 2 Gaudel, Marie-Claude 2 Gibbons, Jeremy 2 Hallerstede, Stefan 2 Hilscher, Martin 2 Jifeng, He 2 Joosten, Stef Maria Mathias 2 Ke, Wei 2 Leino, K. Rustan M. 2 Lermer, Karl 2 Leuschel, Michael 2 Möller, Bernhard 2 Musicante, Martin A. 2 O’Halloran, Colin 2 Oliveira, José Nuno 2 Perna, Juan Ignacio 2 Protsyk, P. P. 2 Schwammberger, Maike 2 Souza Neto, Plácido A. 2 Spivey, J. Michael 2 Spivey, Michael J. 2 Stolz, Volker 2 Wellings, Andy 2 Winter, Kirsten 2 Wolff, Burkhart 2 Wong, Peter Y. H. 2 Zhu, Huibiao 1 Abadi, Aharon 1 Ábrahám, Erika 1 Aguirre, Nazareno M. 1 Ahrendt, Wolfgang 1 Ait-Ameur, Yamine 1 Akgün, Özgür 1 Alcalde, Juan 1 Alvaro, Peter 1 Amálio, Nuno 1 Ambert, Fabrice 1 Ameloot, Tom J. 1 Ammann, Paul 1 Antoniou, Grigoris 1 Apt, Krzysztof Rafal 1 Arenas, Aurelio 1 Arthan, Rob D. 1 Atkinson, Simon 1 Baake, Michael 1 Bailes, Cecily 1 Bainbridge, John R. 1 Banks, Michael J. 1 Barthel, Tobias 1 Basin, David A. 1 Baumeister, Hubert 1 Baxter, James 1 Berendsen, Jasper 1 Berger, Martin J. 1 Berghammer, Rudolf 1 Bessai, Jan 1 Bettaz, Mohamed 1 Bijlsma, Lex 1 Bollin, Andreas 1 Borba, Paulo 1 Börger, Egon 1 Borkowski, Ludwik 1 Bouquet, Fabrice 1 Boute, Raymond T. 1 Bozzelli, Laura 1 Brattka, Vasco 1 Breuillard, Emmanuel ...and 251 more Authors all top 5 Cited in 49 Serials 51 Formal Aspects of Computing 16 Theoretical Computer Science 15 Science of Computer Programming 7 Journal of Logical and Algebraic Methods in Programming 6 Acta Informatica 5 The Journal of Logic and Algebraic Programming 5 Oberwolfach Reports 4 Information Sciences 4 Journal of Automated Reasoning 4 International Journal of Intelligent Systems 4 Formal Methods in System Design 3 Information Processing Letters 3 Real-Time Systems 2 Kybernetes 2 Rendiconti dell’Istituto di Matematica dell’Università di Trieste 2 Software. Practice & Experience 2 Journal of Symbolic Computation 2 Information and Computation 2 Cybernetics and Systems Analysis 2 Visnyk. Seriya: Fizyko-Matematychni Nauky. Kyïvs’kyĭ Universytet Imeni Tarasa Shevchenka 2 Theory and Practice of Logic Programming 2 Journal of Applied Logic 2 Logical Methods in Computer Science 1 ACM Computing Surveys 1 Artificial Intelligence 1 Computer Physics Communications 1 The Mathematical Intelligencer 1 Fundamenta Mathematicae 1 Journal of Pure and Applied Algebra 1 Studia Logica 1 Cybernetics and Systems 1 Annals of Pure and Applied Logic 1 Journal of Computer Science and Technology 1 Mathematical and Computer Modelling 1 JETAI. Journal of Experimental & Theoretical Artificial Intelligence 1 International Journal of Computer Mathematics 1 Distributed Computing 1 Theory of Computing Systems 1 European Series in Applied and Industrial Mathematics (ESAIM): Proceedings 1 Abstract and Applied Analysis 1 Chicago Journal of Theoretical Computer Science 1 RAIRO. Theoretical Informatics and Applications 1 Concurrency and Computation: Practice & Experience 1 ACM Transactions on Computational Logic 1 Lecture Notes in Computer Science 1 Scientia Iranica. Transactions D: Computer Science & Engineering, Electrical Engineering 1 Central European Journal of Computer Science 1 Frontiers of Computer Science in China 1 Frontiers of Computer Science all top 5 Cited in 28 Fields 211 Computer science (68-XX) 36 Mathematical logic and foundations (03-XX) 8 General and overarching topics; collections (00-XX) 4 Category theory; homological algebra (18-XX) 4 Operations research, mathematical programming (90-XX) 3 Combinatorics (05-XX) 3 General algebraic systems (08-XX) 3 Number theory (11-XX) 2 Algebraic geometry (14-XX) 2 Group theory and generalizations (20-XX) 2 Measure and integration (28-XX) 2 Dynamical systems and ergodic theory (37-XX) 2 Algebraic topology (55-XX) 2 Biology and other natural sciences (92-XX) 2 Systems theory; control (93-XX) 2 Mathematics education (97-XX) 1 History and biography (01-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 Associative rings and algebras (16-XX) 1 Ordinary differential equations (34-XX) 1 Partial differential equations (35-XX) 1 Convex and discrete geometry (52-XX) 1 General topology (54-XX) 1 Manifolds and cell complexes (57-XX) 1 Probability theory and stochastic processes (60-XX) 1 Numerical analysis (65-XX) 1 Quantum theory (81-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) Citations by Year