The primary aim of this book is to make the principles of program derivation
from specifications accessible to undergraduates early in their study of
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.