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**: 18,279

The Craft of Programming

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

Terms and Conditions:

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.

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.

Tweet

About The Author(s)

No information is available for this author.

Book Categories

Computer Science
Introduction to Computer Science
Introduction to Computer Programming
Algorithms and Data Structures
Artificial Intelligence
Computer Vision
Machine Learning
Neural Networks
Game Development and Multimedia
Data Communication and Networks
Coding Theory
Computer Security
Information Security
Cryptography
Information Theory
Computer Organization and Architecture
Operating Systems
Image Processing
Parallel Computing
Concurrent Programming
Relational Database
Document-oriented Database
Data Mining
Big Data
Data Science
Digital Libraries
Compiler Design and Construction
Functional Programming
Logic Programming
Object Oriented Programming
Formal Methods
Software Engineering
Agile Software Development
Information Systems
Geographic Information System (GIS)

Mathematics
Mathematics
Algebra
Abstract Algebra
Linear Algebra
Number Theory
Numerical Methods
Precalculus
Calculus
Differential Equations
Category Theory
Proofs
Discrete Mathematics
Theory of Computation
Graph Theory
Real Analysis
Complex Analysis
Probability
Statistics
Game Theory
Queueing Theory
Operations Research
Computer Aided Mathematics

Supporting Fields
Web Design and Development
Mobile App Design and Development
System Administration
Cloud Computing
Electric Circuits
Embedded System
Signal Processing
Integration and Automation
Network Science
Project Management

Operating System
Programming/Scripting
Ada
Assembly
C / C++
Common Lisp
Forth
Java
JavaScript
Lua
Rexx
Microsoft .NET
Perl
PHP
R
Python
Rebol
Ruby
Scheme
Tcl/Tk

Miscellaneous
Sponsors