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).

• Preface ix1 A Science of Computing 11.1 Debugging 21.2 Testing a Correct Program 31.3 Testing an Incorrect Program 51.4 Correct by Construction 62 A Searching Problem and Its Solution 92.1 Problem Statement 92.2 Problem Solution 112.3 Proof of Correctness 122.4 What, Why and How 142.5 Exercises 152.6 Summary 213 Calculational Proof 233.1 The Nature of Proof 233.2 Construction versus Verification 263.3 Formatting Calculations 313.3.1 Basic Structure 313.3.2 Hints 323.3.3 Relations between Steps 343.3.4 ‘IT’ and ‘Only If’ 363.4 A Classic Example 373.5 Summary 394 Implementation Issues 414.1 Binary Search 414.1.1 Implementation 444.2 Verifying Correctness—A Taster 454.3 Summary 525 Calculational Logic: Part 1 535.1 Logical Connectives 545.2 Boolean Equality 565.3 Examples of the Associativity of Equivalence 595.4 Continued Equivalences 615.5 The Island of Knights and Knaves 635.6 Negation 655.7 Summary 686 Number Conversion 716.1 The Floor Function 716.2 Properties of Floor 736.3 Indirect Equality 756.4 Rounding Off 776.5 Summary 807 Calculational Logic: Part 2 837.1 Disjunction 837.2 Conjunction 857.3 Implication 887.3.1 Definitions and Basic Properties 897.3.2 Replacement Rules 907.4 Exercises: Logic Puzzles 937.5 Summary 968 Maximum and Minimum 978.1 Definition of Maximum 978.2 Using Indirect Equality 988.3 Exercises 1018.4 Summary 1039 The Assignment Statement 1059.1 Hoare Triples 1059.2 Ghost Variables 1079.3 Hoare Triples as Program Specifications 1099.4 Assignment Statements 1129.5 The Assignment Axiom 1139.6 Calculating Assignments 1159.7 Complications 1189.8 Summary 11910 Sequential Composition and Conditional Statements 12110.1 Sequential Composition 12110.2 The skip Statement 12310.3 Conditional Statements 12410.4 Reasoning about Conditional Statements 12610.5 Constructing Conditional Statements 13010.6 Combining the Rules 13210.7 Summary 13611 Quantifiers 13711.1 DotDotDot and Sigmas 13711.2 Introducing Quantifier Notation 14111.2.1 Summation 14111.2.2 Free and Bound Variables 14311.2.3 Properties of Summation 14611.2.4 The Gauss Legend 13111.2.5 Warning 15211.3 Universal and Existential Quantification 15311.3.1 Universal Quantification 15411.3.2 Existential Quantification 15511.3.3 De Morgan’s Rules 15611.4 Quantifier Rules 15611.4.1 The Notation 15711.4.2 Free and Bound Variables 15811.4.3 Dummies 15811.4.4 Range Part 15811.4.5 Trading 15911.4.6 Term Part 15911.4.7 Distributivity Properties 15911.5 Summary 16312 Inductive Proofs and Constructions 16512.1 Patterns and Invariants 16612.2 Mathematical Induction 17012.3 Strong Induction 17512.4 Prom Verification to Construction 17912.5 Summary 18213 Iteration 18313.1 The do-od Statement 18313.2 Constructing Loops 18413.3 Basic Arithmetic Operations 18713.3.1 Summing the Elements of an Array 18713.3.2 Evaluating a Polynomial 18813.3.3 Evaluation of Powers 19113.4 Summary 19514 Sorting and Searching Algorithms 19714.1 The Dutch National Flag 19714.1.1 Problem Statement 19714.1.2 The Solution 19914.1.3 Verifying the Solution 20114.2 Finding the K Smallest Values 20514.2.1 The Specification 20614.2.2 The Algorithm 26814.3 Summary 21215 Remainder Computation 21515.1 Formal Specification 21515.2 Elementary Algorithm 21715.3 The mod and div Functions 21915.3.1 Basic Properties 22115.3.2 Separating mod from ÷ 22315.3.3 Separating ÷ from mod 22415.3.4 Modular Arithmetic 22415.4 Long Division 22815.4.1 Implementing Long Division 22915.4.2 Discarding Auxiliary Variables 23315.5 On-Line Remainder Computation 23415.6 Casting Out Nines 23815.7 Summary 23916 Cyclic Codes 24116.1 Codes and Codewords 24116.2 Boolean Polynomials 24316.3 Dara and Generator Polynomials 24616.4 Long Division 24716.5 Hardware Implementations 24916.6 Summary 253Appendix 255Solutions to Exercises 263References 331Glossary of Symbols 333Index 335

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).

• Preface ix1 A Science of Computing 11.1 Debugging 21.2 Testing a Correct Program 31.3 Testing an Incorrect Program 51.4 Correct by Construction 62 A Searching Problem and Its Solution 92.1 Problem Statement 92.2 Problem Solution 112.3 Proof of Correctness 122.4 What, Why and How 142.5 Exercises 152.6 Summary 213 Calculational Proof 233.1 The Nature of Proof 233.2 Construction versus Verification 263.3 Formatting Calculations 313.3.1 Basic Structure 313.3.2 Hints 323.3.3 Relations between Steps 343.3.4 ‘IT’ and ‘Only If’ 363.4 A Classic Example 373.5 Summary 394 Implementation Issues 414.1 Binary Search 414.1.1 Implementation 444.2 Verifying Correctness—A Taster 454.3 Summary 525 Calculational Logic: Part 1 535.1 Logical Connectives 545.2 Boolean Equality 565.3 Examples of the Associativity of Equivalence 595.4 Continued Equivalences 615.5 The Island of Knights and Knaves 635.6 Negation 655.7 Summary 686 Number Conversion 716.1 The Floor Function 716.2 Properties of Floor 736.3 Indirect Equality 756.4 Rounding Off 776.5 Summary 807 Calculational Logic: Part 2 837.1 Disjunction 837.2 Conjunction 857.3 Implication 887.3.1 Definitions and Basic Properties 897.3.2 Replacement Rules 907.4 Exercises: Logic Puzzles 937.5 Summary 968 Maximum and Minimum 978.1 Definition of Maximum 978.2 Using Indirect Equality 988.3 Exercises 1018.4 Summary 1039 The Assignment Statement 1059.1 Hoare Triples 1059.2 Ghost Variables 1079.3 Hoare Triples as Program Specifications 1099.4 Assignment Statements 1129.5 The Assignment Axiom 1139.6 Calculating Assignments 1159.7 Complications 1189.8 Summary 11910 Sequential Composition and Conditional Statements 12110.1 Sequential Composition 12110.2 The skip Statement 12310.3 Conditional Statements 12410.4 Reasoning about Conditional Statements 12610.5 Constructing Conditional Statements 13010.6 Combining the Rules 13210.7 Summary 13611 Quantifiers 13711.1 DotDotDot and Sigmas 13711.2 Introducing Quantifier Notation 14111.2.1 Summation 14111.2.2 Free and Bound Variables 14311.2.3 Properties of Summation 14611.2.4 The Gauss Legend 13111.2.5 Warning 15211.3 Universal and Existential Quantification 15311.3.1 Universal Quantification 15411.3.2 Existential Quantification 15511.3.3 De Morgan’s Rules 15611.4 Quantifier Rules 15611.4.1 The Notation 15711.4.2 Free and Bound Variables 15811.4.3 Dummies 15811.4.4 Range Part 15811.4.5 Trading 15911.4.6 Term Part 15911.4.7 Distributivity Properties 15911.5 Summary 16312 Inductive Proofs and Constructions 16512.1 Patterns and Invariants 16612.2 Mathematical Induction 17012.3 Strong Induction 17512.4 Prom Verification to Construction 17912.5 Summary 18213 Iteration 18313.1 The do-od Statement 18313.2 Constructing Loops 18413.3 Basic Arithmetic Operations 18713.3.1 Summing the Elements of an Array 18713.3.2 Evaluating a Polynomial 18813.3.3 Evaluation of Powers 19113.4 Summary 19514 Sorting and Searching Algorithms 19714.1 The Dutch National Flag 19714.1.1 Problem Statement 19714.1.2 The Solution 19914.1.3 Verifying the Solution 20114.2 Finding the K Smallest Values 20514.2.1 The Specification 20614.2.2 The Algorithm 26814.3 Summary 21215 Remainder Computation 21515.1 Formal Specification 21515.2 Elementary Algorithm 21715.3 The mod and div Functions 21915.3.1 Basic Properties 22115.3.2 Separating mod from ÷ 22315.3.3 Separating ÷ from mod 22415.3.4 Modular Arithmetic 22415.4 Long Division 22815.4.1 Implementing Long Division 22915.4.2 Discarding Auxiliary Variables 23315.5 On-Line Remainder Computation 23415.6 Casting Out Nines 23815.7 Summary 23916 Cyclic Codes 24116.1 Codes and Codewords 24116.2 Boolean Polynomials 24316.3 Dara and Generator Polynomials 24616.4 Long Division 24716.5 Hardware Implementations 24916.6 Summary 253Appendix 255Solutions to Exercises 263References 331Glossary of Symbols 333Index 335

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).

• Preface ix1 A Science of Computing 11.1 Debugging 21.2 Testing a Correct Program 31.3 Testing an Incorrect Program 51.4 Correct by Construction 62 A Searching Problem and Its Solution 92.1 Problem Statement 92.2 Problem Solution 112.3 Proof of Correctness 122.4 What, Why and How 142.5 Exercises 152.6 Summary 213 Calculational Proof 233.1 The Nature of Proof 233.2 Construction versus Verification 263.3 Formatting Calculations 313.3.1 Basic Structure 313.3.2 Hints 323.3.3 Relations between Steps 343.3.4 ‘IT’ and ‘Only If’ 363.4 A Classic Example 373.5 Summary 394 Implementation Issues 414.1 Binary Search 414.1.1 Implementation 444.2 Verifying Correctness—A Taster 454.3 Summary 525 Calculational Logic: Part 1 535.1 Logical Connectives 545.2 Boolean Equality 565.3 Examples of the Associativity of Equivalence 595.4 Continued Equivalences 615.5 The Island of Knights and Knaves 635.6 Negation 655.7 Summary 686 Number Conversion 716.1 The Floor Function 716.2 Properties of Floor 736.3 Indirect Equality 756.4 Rounding Off 776.5 Summary 807 Calculational Logic: Part 2 837.1 Disjunction 837.2 Conjunction 857.3 Implication 887.3.1 Definitions and Basic Properties 897.3.2 Replacement Rules 907.4 Exercises: Logic Puzzles 937.5 Summary 968 Maximum and Minimum 978.1 Definition of Maximum 978.2 Using Indirect Equality 988.3 Exercises 1018.4 Summary 1039 The Assignment Statement 1059.1 Hoare Triples 1059.2 Ghost Variables 1079.3 Hoare Triples as Program Specifications 1099.4 Assignment Statements 1129.5 The Assignment Axiom 1139.6 Calculating Assignments 1159.7 Complications 1189.8 Summary 11910 Sequential Composition and Conditional Statements 12110.1 Sequential Composition 12110.2 The skip Statement 12310.3 Conditional Statements 12410.4 Reasoning about Conditional Statements 12610.5 Constructing Conditional Statements 13010.6 Combining the Rules 13210.7 Summary 13611 Quantifiers 13711.1 DotDotDot and Sigmas 13711.2 Introducing Quantifier Notation 14111.2.1 Summation 14111.2.2 Free and Bound Variables 14311.2.3 Properties of Summation 14611.2.4 The Gauss Legend 13111.2.5 Warning 15211.3 Universal and Existential Quantification 15311.3.1 Universal Quantification 15411.3.2 Existential Quantification 15511.3.3 De Morgan’s Rules 15611.4 Quantifier Rules 15611.4.1 The Notation 15711.4.2 Free and Bound Variables 15811.4.3 Dummies 15811.4.4 Range Part 15811.4.5 Trading 15911.4.6 Term Part 15911.4.7 Distributivity Properties 15911.5 Summary 16312 Inductive Proofs and Constructions 16512.1 Patterns and Invariants 16612.2 Mathematical Induction 17012.3 Strong Induction 17512.4 Prom Verification to Construction 17912.5 Summary 18213 Iteration 18313.1 The do-od Statement 18313.2 Constructing Loops 18413.3 Basic Arithmetic Operations 18713.3.1 Summing the Elements of an Array 18713.3.2 Evaluating a Polynomial 18813.3.3 Evaluation of Powers 19113.4 Summary 19514 Sorting and Searching Algorithms 19714.1 The Dutch National Flag 19714.1.1 Problem Statement 19714.1.2 The Solution 19914.1.3 Verifying the Solution 20114.2 Finding the K Smallest Values 20514.2.1 The Specification 20614.2.2 The Algorithm 26814.3 Summary 21215 Remainder Computation 21515.1 Formal Specification 21515.2 Elementary Algorithm 21715.3 The mod and div Functions 21915.3.1 Basic Properties 22115.3.2 Separating mod from ÷ 22315.3.3 Separating ÷ from mod 22415.3.4 Modular Arithmetic 22415.4 Long Division 22815.4.1 Implementing Long Division 22915.4.2 Discarding Auxiliary Variables 23315.5 On-Line Remainder Computation 23415.6 Casting Out Nines 23815.7 Summary 23916 Cyclic Codes 24116.1 Codes and Codewords 24116.2 Boolean Polynomials 24316.3 Dara and Generator Polynomials 24616.4 Long Division 24716.5 Hardware Implementations 24916.6 Summary 253Appendix 255Solutions to Exercises 263References 331Glossary of Symbols 333Index 335