The primary aim of this book is to make the principles of program derivation from specifications accessible to undergraduates early in their study of computing science.

The proliferation of personal computers in the home and in schools has meant that there are large numbers of people who have had exposure to using computers and even to 'writing' programs in languages like BASIC. This situation has left many people with the misconception that computing science education is focused upon the coding and debugging of computer programs, whereas this is far from the ideals and objectives of the science. For too long people have tried to learn how to build programs without the support of a rigorous mathematical and logical framework. As a conse quence, the cost of developing high-quality software remains at a premium. There is but one chance of overcoming these problems, and that is to recognize computing science for what it really is, a mathematically-based discipline concerned with the application of rigorous methods for the specification, design, and implementation of computer systems.

It is one thing to be able to write down a few pages of program statements but it is an entirely different matter to produce correct programs that provably satisfy their specifications. That anything less is acceptable merely reflects the stage of development of the discipline. What we have to offer in this book is not something that can cure all these problems. The intent has been to provide an introduction to the level of precision, habits of mind, and modes of reasoning, necessary for producing high-quality verifiable software at a reasonable cost.