Table of Contents

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.