Terms and Conditions:

John C. Reynolds wrote:Do not reproduce these documents for commercial purposes.

Book Excerpts:

The modern computer is so powerful that a casual knowledge of programming suffices for most of its users. However, a variety of circumstances can abruptly require a much deeper understanding: the need to structure a program carefully to avoid being overwhelmed by its complexity, the need to insure reliability beyond what can he achieved by debugging, or the need to utilize computing resources efficiently. Beyond such practical considerations, there is an inherent intellectual satisfaction in mastering the fundamental concepts of programming.

The aim of this book is to provide such mastery concept by concept. For example, the reader is expected to understand proofs of correctness and order-of-magnitude time requirements for simple integer algorithms - such as log n exponentiation - before the concept of arrays is introduced. A similarly thorough understanding of array manipulating algorithms is expected before the introduction of procedures.

The programming language used in this book is Algol W or, more precisely, the subset of Algol W that represents a refinement of Algol 60. Originally the main factor determining this choice was the level of the language. It is sufficiently high-level to provide block structure, including dynamic arrays, and a powerful procedure mechanism, including recursion, call by name, and higher-order procedures. On the other hand, it is sufficiently close to the machine to facilitate the estimation of time and storage requirements. In addition, it has an unusually elegant syntactic structure which permits clean subsetting, and an efficient and unusually error-free implementation.

This book reflects a conviction about the importance of program proving. Ideally at least, a programmer should be able to specify the behavior of his program precisely, and to give a rigorous argument that the program meet its specifications. Of course, such or argument might not be a formal proof in the sense of logic, but it must be an adequate guideline for a formal proof. In other words, a adequately commented program should enable a competent reader to fill in the details of a formal proof in a straightforward manner.

This implies that the programmer should master formal proof methods, not in order to give a formal proof of every program that he writes, but as a firm foundation for rigorous though informal reasoning about programs.