An introduction to Z and formal specifications

The description of information systems using formal, mathematical specifications written in the Z notation, and the refinement of these specifications into rigorously checked designs are described. The author introduces the idea of a formal specification using a simple example: a `birthday book´ in which people´s birthdays can be recorded, and which is able to issue reminders on the appropriate day. The behaviour of this system for correct input is specified; then the schema calculus is used to strengthen the specification into one requiring error reports for incorrect input. The idea of data refinement as the primary means of constructing designs which achieve a formal specification is also demonstrated