Using Z: Specification, Refinement, and Proof
Jim Woodcock, Jim Davies · Medical Entomology and Zoology · 1996
* Introduction. * Propositional Logic. * Predicate Logic. * Equality and Definite Description. * Sets. * Definitions. * Relations. * Functions. * Sequences. * Free Types. * Schemas Schema Operators. * Promotion, Preconditons. * Data Refinement. * Relaxing and Unwinding Data Refinement and Z. * Applications of Data Refinement. * The Refinement Calculus. * A File System. * A Telecommunications Protocol. * An Operating System Scheduler: A Bounded Buffer Module. * An Unordered Set Module. * A Save Area. * Solutions to Exercises. * Appendices. * Bibliography. * Index.