The Craft of Programming

The Craft of Programming

A textbook on programming with emphasis on specification and proof of programs. Includes the results of author's own research.

Publication date: 01 Jun 1981

ISBN-10: 0131888625

ISBN-13: n/a

Paperback: 434 pages

Views: 14,031

Type: N/A

Publisher: Prentice Hall

License: n/a

Post time: 06 Dec 2006 07:57:35

The Craft of Programming

The Craft of Programming A textbook on programming with emphasis on specification and proof of programs. Includes the results of author's own research.
Tag(s): Formal Methods
Publication date: 01 Jun 1981
ISBN-10: 0131888625
ISBN-13: n/a
Paperback: 434 pages
Views: 14,031
Document Type: N/A
Publisher: Prentice Hall
License: n/a
Post time: 06 Dec 2006 07:57:35
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.




About The Author(s)


No information is available for this author.

John C. Reynolds

No information is available for this author.


Book Categories
Sponsors
Icons8, a free icon pack