Z
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.
Keywords for this software
References in zbMATH (referenced in 279 articles , 1 standard article )
Showing results 1 to 20 of 279.
Sorted by year (- Cristiá, Maximiliano; Rossi, Gianfranco: Automated proof of Bell-LaPadula security properties (2021)
- Foster, Simon; Ye, Kangfeng; Cavalcanti, Ana; Woodcock, Jim: Automated verification of reactive and concurrent programs by calculation (2021)
- Jackson, Marcel; Stokes, Tim: Override and update (2021)
- Foster, Simon; Cavalcanti, Ana; Canham, Samuel; Woodcock, Jim; Zeyda, Frank: Unifying theories of reactive design contracts (2020)
- Kahl, Wolfram: Calculational relation-algebraic proofs in the teaching tool \textscCalcCheck (2020)
- Lahouij, Aida; Hamel, Lazhar; Graiet, Mohamed; el Ayeb, Béchir: An Event-B based approach for cloud composite services verification (2020)
- Apt, Krzysztof R.; Olderog, Ernst-Rüdiger: Fifty years of Hoare’s logic (2019)
- Lin, Yuhui; Bundy, Alan; Grov, Gudmund; Maclean, Ewen: Automating Event-B invariant proofs by rippling and proof patching (2019)
- Ribeiro, Pedro; Cavalcanti, Ana: Angelic processes for CSP via the UTP (2019)
- Barthel, Tobias (ed.); Krause, Henning (ed.); Stojanoska, Vesna (ed.): Mini-workshop: Chromatic phenomena and duality in homotopy theory and representation theory. Abstracts from the mini-workshop held March 4--10, 2018 (2018)
- Bessai, Jan; Chen, Tzu-Chun; Dudenhefner, Andrej; Düdder, Boris; De’liguoro, Ugo; Rehof, Jakob: Mixin composition synthesis based on intersection types (2018)
- Brattka, Vasco (ed.); Downey, Rodney G. (ed.); Knight, Julia F. (ed.); Lempp, Steffen (ed.): Computability theory. Abstracts from the workshop held January 7--13, 2018 (2018)
- Joosten, Sebastiaan J. C.: Finding models through graph saturation (2018)
- Joosten, Stef: Relation algebra as programming language using the Ampersand compiler (2018)
- Schwammberger, Maike: An abstract model for proving safety of autonomous urban traffic (2018)
- Ahrendt, Wolfgang; Chimento, Jesús Mauricio; Pace, Gordon J.; Schneider, Gerardo: Verifying data- and control-oriented properties combining static and runtime verification: theory and tools (2017)
- Baake, Michael (ed.); Damanik, David (ed.); Kellendonk, Johannes (ed.); Lenz, Daniel (ed.): Spectral structures and topological methods in mathematical quasicrystals. Abstracts from the workshop held October 1--7, 2017 (2017)
- Bjørner, Dines: Manifest domains: analysis and description (2017)
- Breuillard, Emmanuel (ed.); Hochman, Michael (ed.); Shmerkin, Pablo (ed.): Working session: Additive combinatorics, entropy, and fractal geometry. Abstracts from the working session held October 8--13, 2017 (2017)
- Buss, Samuel R. (ed.); Iemhoff, Rosalie (ed.); Kohlenbach, Ulrich (ed.); Rathjen, Michael (ed.): Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 (2017)