This paper provides an introduction to the description of information systems using formal, mathematical specifications written in the Z notation, and to the refinement of these specifications into rigorously checked designs. The first part introduces the idea of a formal specification using a simple example: that of 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 first; then the schema calculus is used to strengthen the specification into one requiring error reports for incorrect input. The second part of the paper introduces the idea of data refinement as the primary means of constructing designs which achieve a formal specification. Refinement is presented through the medium of two examples: the first is a direct implementation of the birthday book from part one; and the second is a simple checkpoint facility, which allows the current state of a database to be saved and later restored. A Pascal-like programming language is used to show the code for some of the operations in the examples.