## A Practical Theory of ProgrammingThere are several theories of programming. The first usable theory, often called "Hoare's Logic", is still probably the most widely known. In it, a specification is a pair of predicates: a precondition and postcondition (these and all technical terms will be defined in due course). Another popular and closely related theory by Dijkstra uses the weakest precondition predicate transformer, which is a function from programs and postconditions to preconditions. lones's Vienna Development Method has been used to advantage in some industries; in it, a specification is a pair of predicates (as in Hoare's Logic), but the second predicate is a relation. Temporal Logic is yet another formalism that introduces some special operators and quantifiers to describe some aspects of computation. The theory in this book is simpler than any of those just mentioned. In it, a specification is just a boolean expression. Refinement is just ordinary implication. This theory is also more general than those just mentioned, applying to both terminating and nonterminating computation, to both sequential and parallel computation, to both stand-alone and interactive computation. And it includes time bounds, both for algorithm classification and for tightly constrained real-time applications. |

### What people are saying - Write a review

User Review - Flag as inappropriate

Of the many theories about the mathematical properties of computer programs this is by far the simplest, yet most comprehensive. The book starts by introducing a simple formal framework for logical calculations which are then used to reason about program properties.

Unfortunately this book, written as a class text for university students, is the only reference for the theory.

Note that the much revised and updated second edition of the book is available for free online: http://www.cs.toronto.edu/~hehner/aPToP/

Robert Will

### Contents

Quick Tour | 1 |

Acknowledgments | 2 |

Basic Theories | 3 |

Axioms and Proof Rules | 6 |

Expression and Proof Format | 8 |

Formalization | 11 |

Number Theory | 12 |

Character Theory | 13 |

Function Refinement | 89 |

Recursive Definition | 91 |

Least FixedPoints | 94 |

Recursive Data Construction | 95 |

Recursive Program Definition | 98 |

Recursive Program Construction | 99 |

Loop Definition | 100 |

Limits | 101 |

Basic Data Structures | 14 |

Set Theory | 17 |

String Theory | 18 |

List Theory | 21 |

Multidimensional Structures | 23 |

Function Theory | 24 |

Abbreviated Function Notations | 26 |

Scope and Substitution | 27 |

Quantifiers | 28 |

Function Fine Points | 30 |

Function Inclusion and Equality | 32 |

Function Composition | 33 |

List as Function | 35 |

Program Theory | 36 |

Specifications | 37 |

Specification Notations | 38 |

Specification Laws | 40 |

Refinement | 42 |

Conditions | 43 |

Programs | 45 |

Program Development | 47 |

List Summation | 48 |

Binary Exponentiation | 50 |

Time | 51 |

Recursive Time | 53 |

Termination | 55 |

Linear Search | 57 |

Binary Search | 58 |

Fast Exponentiation | 63 |

Fibonacci Numbers | 65 |

Robustness | 67 |

Refinement in Place | 68 |

Programming Language | 70 |

Variable Suspension | 71 |

Data Structures | 72 |

Records | 74 |

Repeat Loop | 75 |

TwoDimensional Search | 77 |

For Loop | 79 |

Go To | 80 |

Time Dependence | 81 |

Assertions | 82 |

Subprogram | 83 |

Function | 84 |

Procedure | 85 |

Alias | 86 |

Functional Programming | 87 |

Theory Design and Implementation | 102 |

DataStack Implementation | 103 |

Simple DataStack Theory | 104 |

DataQueue Theory | 105 |

DataTree Theory | 107 |

Program Theories | 110 |

ProgramStack Implementation | 111 |

ProgramQueue Theory | 112 |

Specification by Implementation | 115 |

Data Transformation | 116 |

Concurrency | 120 |

Independent Composition | 121 |

Laws of Independent Composition | 123 |

List Concurrency | 124 |

Circuit Design | 125 |

Found Concurrency | 127 |

Buffer | 128 |

Insertion Sort | 129 |

Communication | 131 |

Implementability | 132 |

Communication Timing | 134 |

Recursively Defined Communication | 135 |

Merge | 136 |

Monitor | 137 |

Reaction Controller | 139 |

Communicating Processes | 140 |

Channel Declaration | 141 |

Deadlock | 142 |

Power Series Multiplication | 143 |

Exercises | 149 |

Basic Data Structures | 155 |

Function Theory | 158 |

Program Theory | 162 |

Programming Language | 182 |

Recursive Definition | 185 |

Theory Design and Implementation | 192 |

Concurrency | 197 |

Communication | 199 |

Reference | 204 |

Sources | 213 |

215 | |

219 | |

Axioms and Laws | 229 |

Symbols and Names | 241 |

Precedence | 243 |

### Other editions - View all

### Common terms and phrases

antitheorem apply assignment binary logarithm boolean expression Boolean Theory called catenation ceil log j-h channel Chapter computation construction and induction constructor data structure data transformation defined dependent composition distributivity div h+j domain Edsger Dijkstra element empty equal exact precondition example execution Fibonacci final value fixed-point fixed-point construction formally function Function Composition functional programming given list greatest common divisor idempotent illus imperative programming implementation implementer's variables induction axiom input integer variable loop nat+ natural number natural variables notation null operands operators output postcondition predicate problem processes Program Theory program to find program-stack theory programming languages proof prove push quantifier queue recursive construction refinement replace result satisfy segment sequence solution sorted list specification stack strings Substitution Law theorem Tony Hoare tree truth table universal quantification Write a program