# A Practical Theory of Programming

Springer Science & Business Media, Aug 6, 1993 - Computers - 247 pages
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