Logical Derivation of Computer Programs
Will be published approx. on 1. May 1999
Book
Hardback
200 pages
978-1-871516-98-2 (ISBN)
Description
This text presents a language-based logic for procedures to derive computer programs from formal specifications. This approach is based upon design philosophy, and the author has set out to use language that is easy to understand. The method has also been class-tested throughout its development, and features examples, solved exercises and explanations.
More details
Language
English
Place of publication
United Kingdom
Publishing group
Intellect
Target group
College/higher education
Professional and scholarly
ISBN-13
978-1-871516-98-2 (9781871516982)
Copyright in bibliographic data and cover images is held by Nielsen Book Services Limited or by the publishers or by their respective licensors: all rights reserved.
Schweitzer Classification
Content
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
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