Covers the main areas of formal specification in Z at an introductory level. The explanations of the mathematics of Z are interleaved with the development of an example specification. Exercises are included throughout and sample solutions are provided.