Logical Derivation of Computer Programs
Logical Derivation of Computer Programs (Book)
This book presents a method that constitutes a powerful new tool for creating error-free programs and showing students a rigorous mathematical approach to programming.
As a textbook for a one-semester course on program derivation, the text develops a fresh new language-based logic for procedures to derie computer programs from formal specifications. This approach is based upon design philosophy, hence strongly related to the students' interests and background.
The book is designed to be challenging while not being difficult to understand by students exploring the field. Class-tested by the author throughout its development: the book has down-to-earth explanations, detailed and cogent examples, along with solved exercises. This material has not been previously published, and is not overly influenced by the computer science literature.
Edition
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