'… this reviewer cannot imagine a book better suited to inspiring the sceptical hacker into believing that there is some genuine value in formal methods.' R. H. Banach, Axis

• Part I. Why Z?: 1. Formal methods; 2. Why use formal methods?; 3. Formal methods and project management; Part II. Introducing Z: 4. What is Z?; 5. A first example in Z; 6. From prose to Z: control console; 7. Introducing schemas: text editor; Part III. Elements of Z: 8. Elements; 9. Structure; 10. Logic; 11. Synthesis; 12. Schemas and schema calculus; 13. Schema types and bindings; 14. Generic definitions and free types; 15. Formal reasoning; Part IV. Studies in Z: 16. Document control system; 17. Text processing; 18. Eight queens; 19. Computer graphics and computational geometry; 20. Rule-based programming; 21. Graphical user interface; 22. Safety-critical protection system; 23. Modelling large systems; 24. Concurrency and real time; 25. Object-oriented programming; Part V. From Z to Code: 26. Program derivation and formal verification; 27. From Z to code.

'… this reviewer cannot imagine a book better suited to inspiring the sceptical hacker into believing that there is some genuine value in formal methods.' R. H. Banach, Axis

• Part I. Why Z?: 1. Formal methods; 2. Why use formal methods?; 3. Formal methods and project management; Part II. Introducing Z: 4. What is Z?; 5. A first example in Z; 6. From prose to Z: control console; 7. Introducing schemas: text editor; Part III. Elements of Z: 8. Elements; 9. Structure; 10. Logic; 11. Synthesis; 12. Schemas and schema calculus; 13. Schema types and bindings; 14. Generic definitions and free types; 15. Formal reasoning; Part IV. Studies in Z: 16. Document control system; 17. Text processing; 18. Eight queens; 19. Computer graphics and computational geometry; 20. Rule-based programming; 21. Graphical user interface; 22. Safety-critical protection system; 23. Modelling large systems; 24. Concurrency and real time; 25. Object-oriented programming; Part V. From Z to Code: 26. Program derivation and formal verification; 27. From Z to code.