Preface ix
1 A Science of Computing 1
1.1 Debugging 2
1.2 Testing a Correct Program 3
1.3 Testing an Incorrect Program 5
1.4 Correct by Construction 6
2 A Searching Problem and Its Solution 9
2.1 Problem Statement 9
2.2 Problem Solution 11
2.3 Proof of Correctness 12
2.4 What, Why and How 14
2.5 Exercises 15
2.6 Summary 21
3 Calculational Proof 23
3.1 The Nature of Proof 23
3.2 Construction versus Verification 26
3.3 Formatting Calculations 31
3.3.1 Basic Structure 31
3.3.2 Hints 32
3.3.3 Relations between Steps 34
3.3.4 ‘IT’ and ‘Only If’ 36
3.4 A Classic Example 37
3.5 Summary 39
4 Implementation Issues 41
4.1 Binary Search 41
4.1.1 Implementation 44
4.2 Verifying Correctness—A Taster 45
4.3 Summary 52
5 Calculational Logic: Part 1 53
5.1 Logical Connectives 54
5.2 Boolean Equality 56
5.3 Examples of the Associativity of Equivalence 59
5.4 Continued Equivalences 61
5.5 The Island of Knights and Knaves 63
5.6 Negation 65
5.7 Summary 68
6 Number Conversion 71
6.1 The Floor Function 71
6.2 Properties of Floor 73
6.3 Indirect Equality 75
6.4 Rounding Off 77
6.5 Summary 80
7 Calculational Logic: Part 2 83
7.1 Disjunction 83
7.2 Conjunction 85
7.3 Implication 88
7.3.1 Definitions and Basic Properties 89
7.3.2 Replacement Rules 90
7.4 Exercises: Logic Puzzles 93
7.5 Summary 96
8 Maximum and Minimum 97
8.1 Definition of Maximum 97
8.2 Using Indirect Equality 98
8.3 Exercises 101
8.4 Summary 103
9 The Assignment Statement 105
9.1 Hoare Triples 105
9.2 Ghost Variables 107
9.3 Hoare Triples as Program Specifications 109
9.4 Assignment Statements 112
9.5 The Assignment Axiom 113
9.6 Calculating Assignments 115
9.7 Complications 118
9.8 Summary 119
10 Sequential Composition and Conditional Statements 121
10.1 Sequential Composition 121
10.2 The skip Statement 123
10.3 Conditional Statements 124
10.4 Reasoning about Conditional Statements 126
10.5 Constructing Conditional Statements 130
10.6 Combining the Rules 132
10.7 Summary 136
11 Quantifiers 137
11.1 DotDotDot and Sigmas 137
11.2 Introducing Quantifier Notation 141
11.2.1 Summation 141
11.2.2 Free and Bound Variables 143
11.2.3 Properties of Summation 146
11.2.4 The Gauss Legend 131
11.2.5 Warning 152
11.3 Universal and Existential Quantification 153
11.3.1 Universal Quantification 154
11.3.2 Existential Quantification 155
11.3.3 De Morgan’s Rules 156
11.4 Quantifier Rules 156
11.4.1 The Notation 157
11.4.2 Free and Bound Variables 158
11.4.3 Dummies 158
11.4.4 Range Part 158
11.4.5 Trading 159
11.4.6 Term Part 159
11.4.7 Distributivity Properties 159
11.5 Summary 163
12 Inductive Proofs and Constructions 165
12.1 Patterns and Invariants 166
12.2 Mathematical Induction 170
12.3 Strong Induction 175
12.4 Prom Verification to Construction 179
12.5 Summary 182
13 Iteration 183
13.1 The do-od Statement 183
13.2 Constructing Loops 184
13.3 Basic Arithmetic Operations 187
13.3.1 Summing the Elements of an Array 187
13.3.2 Evaluating a Polynomial 188
13.3.3 Evaluation of Powers 191
13.4 Summary 195
14 Sorting and Searching Algorithms 197
14.1 The Dutch National Flag 197
14.1.1 Problem Statement 197
14.1.2 The Solution 199
14.1.3 Verifying the Solution 201
14.2 Finding the K Smallest Values 205
14.2.1 The Specification 206
14.2.2 The Algorithm 268
14.3 Summary 212
15 Remainder Computation 215
15.1 Formal Specification 215
15.2 Elementary Algorithm 217
15.3 The mod and div Functions 219
15.3.1 Basic Properties 221
15.3.2 Separating mod from ÷ 223
15.3.3 Separating ÷ from mod 224
15.3.4 Modular Arithmetic 224
15.4 Long Division 228
15.4.1 Implementing Long Division 229
15.4.2 Discarding Auxiliary Variables 233
15.5 On-Line Remainder Computation 234
15.6 Casting Out Nines 238
15.7 Summary 239
16 Cyclic Codes 241
16.1 Codes and Codewords 241
16.2 Boolean Polynomials 243
16.3 Dara and Generator Polynomials 246
16.4 Long Division 247
16.5 Hardware Implementations 249
16.6 Summary 253
Appendix 255
Solutions to Exercises 263
References 331
Glossary of Symbols 333
Index 335
