Much current research in computer science is concerned with two
questions: is a program correct? And how can we improve a correct
program preserving correctness? This latter question is known as the
refinement of programs and the purpose of this book is to consider these
questions in a formal setting. In fact, correctness turns out to be a
special case of refinement and so the focus is on refinement. Although a
reasonable background knowledge is assumed from mathematics and CS, the
book is a self-contained introduction suitable for graduate students and
researchers coming to this subject for the first time. There are
numerous exercises provided of varying degrees of challenge.