xix, 374 pages : 25 cm
This tutorial introduction to Z takes as its starting point the practical uses of this formal specification language. Case studies are used throughout the text to illustrate all aspects of Z. This edition includes new information on how to relate Z specifications to actual program codes
Includes bibliographical references (pages 357-362) and index
1. Introduction. 1.1. What is Z? 1.2. Specification Foretaste. 1.3. Numbers -- 2. First-order Logic. 2.1. Propositional Calculus. 2.2. Predicate Calculus -- 3. Set Theory. 3.1. Ways of Making Sets. 3.2. Relations between Sets (and their Members). 3.3. Some Special Sets. 3.4. Operations on Sets -- 4. Internal Telephone Directory. 4.2. Cartesian Products and Relations. 4.3. The State Space. 4.4. Adding an Entry to the Database. 4.5. Interrogating the Database by Person. 4.6. Interrogating the Database by Number. 4.7. Removing an Entry from the Database. 4.8. Someone Joining the University. 4.9. Someone Leaving the University. 4.10. Specifying a User-interface. 4.11. Presenting a Formal Specification -- 5. More about Relations and Schemas. 5.1. Relations. 5.2. Schemas -- 6. Functions. 6.2. Specifying a Weather Map. 6.3. Constrained Functions. 6.4. Function Definition. 6.5. Modelling Arrays -- 7. Sequences. 7.1. Fundamental Ideas. 7.2. Defining Sequences. 7.3. Sequence Manipulating Functions
8. Bags. 8.2. Bag Manipulating Functions. 8.3. A Specification of Sorting. 8.4. The Specification of a Vending Machine -- 9. Free Types. 9.2. Lists as a Free Type. 9.3. Specifying Sequence Proofs. 9.4. The Formal Treatment of Free Types -- 10. Formal Proof. 10.1. Propositional Calculus. 10.2. Predicate Calculus. 10.3. Theorems, Sequents and Themata -- 11. Rigorous Proof. 11.2. Reasoning about Sets. 11.3. Reasoning about Tuples. 11.4. Mathematical Induction. 11.5. Induction for Sequences -- 12. Immanent Reasoning. 12.2. Specifying a Classroom. 12.3. Schemas and Formulas. 12.4. The Initiation Proof Obligation. 12.5. Constructing Theories about Specifications. 12.6. Investigating Preconditions. 12.7. Totality. 12.8. Operation Refinement -- 13. Reification and Decomposition. 13.2. Modelling Sets by Sequences. 13.3. Reification and Decomposition using Schemas -- 14. Floyd-Hoare Logic. 14.2. Hoare Triples. 14.3. Start Sequents and Themata. 14.4. Total Correctness. 14.5. Using Mathematical Variables
14.6. Verification Conditions -- 15. Getting to Program Code. 15.1. The Transformation Recipe. 15.2. Modelling a Simple Bank Account. 15.3. A Sales Database -- 16. Two Small Case Studies. 16.1. The Bill of Materials Problem. 16.2. A Route Planner -- 17. Wing's Library Problem. 17.2. Basic Types and User-defined Sets. 17.3. The State of the System. 17.4. The Operations -- 18. Partial Specification of a Text-editor. 18.2. Basic Types. 18.3. The State Space. 18.4. The Operations. 18.5. The Doc2 State. 18.6. The Doc3 Model -- 19. Animation using Miranda. 19.2. The Animation -- 20. Methods of Definition. 20.1. Axiomatic Description. 20.2. Generic Definition. 20.3. Schema Definition -- 21. Formal Definitions. 21.1. Sets. 21.2. Relations. 21.3. Functions. 21.4. Sequences. 21.5. Bags -- 22. Rules and Obligations. 22.1. First-order Logic. 22.2. Reasoning about Sets. 22.3. Reasoning about Tuples. 22.4. Floyd-Hoare Logic. 22.5. Induction. 22.6. Proof Obligations for Refinement
App. A Variable Conventions -- App. B Answers to Exercises -- App. C Glossary of Terms -- App. D Glossary of Symbols
Legacy 2018

ia/zintroductiontof0000dill.pdf

Antoni Diller

Jossey-Bass, Incorporated Publishers

John Wiley & Sons, Incorporated

WILEY COMPUTING Publisher

United States, United States of America

2nd ed, Chichester [etc, 1994

2 Sub edition, June 16, 1994

2, PS, 1994

Includes bibliographical references (p. 357-362) and index.

<p>Offers a thorough and comprehensive tutorial introduction to Z. Uses standard notation with practical exercises and clear descriptions and explanations. Contains information on how to relate Z specifications to actual program code and is enhanced to reflect the most current language standards.</p>


<p>A thorough and comprehensive tutorial introduction to Z. The author uses case studies to vividly illustrate all aspects of Z. With practical exercises and clear descriptions and explanations throughout, this updated edition will be required reading for all students and software engineers learning Z.
</p>

Z is a language, but knowing this does not tell you very much about it because there are many different kinds of language, such as natural language and programming language.

2023-06-28