A Practical Theory of Programming

Front Cover
Springer Science & Business Media, Aug 6, 1993 - Computers - 247 pages
2 Reviews
There 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
Bibliography
215
Index
219
Axioms and Laws
229
Symbols and Names
241
Precedence
243
Copyright

Other editions - View all

Common terms and phrases

References to this book

All Book Search results »

Bibliographic information