Preface ................................................................................................. i

1 Logical Proofs
1.1 BACKGROUND ............................................................................................................ I
1.2 LOGICAL PROOF SYSTEMS ........................................................................................ 2
1.3 PROOFS IN BOOLEAN ALGEBRA ................................................................................. 5
1.4 PROVING PROPOSITIONAL CALCULUS ....................................................................... 10
1.5 TAUTOLOGIES ............................................................................................................. 13
1.6 OTHER FORMS OF LOGICAL PROOF ........................................................................... 14
1.7 QUANTIFIERS ............................................................................................................. 16
1.8 FOUR AXIOMS OF SET THEORY ................................................................................. 20
1.9 SET-THEORETIC IDENTITIES ....................................................................................... 22
1.10 PROVING THE ALGEBRA OF SETS ............................................................................ 24
1.11 DECOMPOSITION OF PROOFS .................................................................................. 29
EXERCISES ....................................................................................................................... 33

2 Mathematical Induction
2.1 THE SET OF NATURAL NUMBERS .............................................................................. 37
2.2 DEFINING ARITHMETIC .............................................................................................. 41
2.3 HIGHER-ORDER INDUCTIVE DEFINITIONS .................................................................. 45
2.4 EVOLVERS AND ITERATION ....................................................................................... 47
2.5 SET-THEORETIC EVOLVERS ....................................................................................... 50
2.6 THE ALGEBRA OF RELATIONS ................................................................................... 52
2.7 INDUCTIVE PROOFS ................................................................................................... 54
2.8 THE ALGEBRA OF LISTS ............................................................................................ 58
EXERCISES ...................................................................................................................... 61

3 Traditional Programming
3.1 INTRODUCTION .......................................................................................................... 65
3.2 A RUDIMENTARY PROGRAMMING LANGUAGE .......................................................... 67
3.3 INVENTION OF PROGRAMS ........................................................................................ 69
3.4 FORMALIZING PROCEDURAL SPECIFICATIONS ......................................................... 74
3.5 INFORMAL VERIFICATION ARGUMENTS .................................................................... 76
EXERCISES ....................................................................................................................... 79

4 A Logic for Procedures
4.1 INTRODUCTION .......................................................................................................... 83
4.2 PROCEDURAL EQUIVALENCE .................................................................................... 84
4.3 THE SUBSTITUTION AND LEIBNITZ RULES ................................................................. 86
4.4 REWRITING RULES FOR ASSIGNMENTS .................................................................... 90
4.5 CONDITIONAL EXPRESSIONS AND BRANCHES .......................................................... 95
4.6 ITERATION AND FOR-LOOPS ..................................................................................... 99
4.7 HIGH-LEVEL REWRITING RULES ................................................................................ 103
4.8 RECURSIVE PROCEDURES ......................................................................................... 109
4.9 TAIL RECURSION AND WHILE-LOOPS ........................................................................ 113
4.10 PROGRAMS AND PROCEDURE CALL REPLACEMENT .............................................. 117
EXERCISES ....................................................................................................................... 122

5 Examples of Program Derivation
5.1 PROGRA.MMING THE ALGEBRA OF SETS .................................................................... 127
5.2 PROGRAMMING PREDICATES .................................................................................... 132
5.3 PROGRAMMING THE ALGEBRA OF RELATIONS ......................................................... 139
5.4 PROGRAMMING EQUIVALENCE RELATIONS AND PARTITIONS .................................. 144
5.5 PROGRAMMING THE TRANSITIVE CLOSURE ............................................................. 149
5.6 EMBEDDING SPECIFICATIONS .................................................................................... 151
5.7 PROGRAMMING NATURAL NUMBER ARITHMETIC ..................................................... 152
5.8 PROGRAMMING THE ALGEBRA OF LISTS ................................................................... 161
5.9 COMPUTING SETS USING ONE-ONE LISTS .................................................................. 164
5.10 SEARCHING AND SORTING LISTS ............................................................................. 167
EXERCISES ....................................................................................................................... 174

Bibliography ...................................................................................................................... 179

A The Procedural Rewriting Rules ............................................................................. 181

B Solution of Even-Numbered Exercises ................................................................. 185

Index .................................................................................................................................... 205