Program Construction: Calculating Implementations from Specifications

Table of Contents:
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

About the Author :
Roland Backhouse leads the Foundations of Programming research group at the University of Nottingham. He returned to the UK in 1999 after spending 13 years in the Netherlands, 9 of which as professor at Eindhoven University of Technology (the institution that pioneered the style of reasoning and construction of programs that forms the basis for this book).