Preface
CHAPTER 1 COMPUTABILITY
INTRODUCTION 1
1-1 FINITE AUTOMATA 2
1-1.1 Regular Expressions 3
1-1.2 Finite Automata 7
1-1.3 Transition Graphs 9
1-1.4 Kleene's Theorem 11
1-1.5 The Equivalence Theorem 17
1-2 TURING MACHINES 20
1-2.1 Turing Machines 21
1-2.2 Post Machines 24
1-2.3 Finite Machines with Pushdown Stores 29
1-2.4 N ondeterminism 35
1-3 TURING MACHINES AS ACCEPTORS 37
1-3.1 Recursively Enumerable Sets 38
1-3.2 Recursive Sets 39
1-3.3 Formal Languages 41
1-4 TURING MACHINES AS GENERATORS 43
1-4.1 Primitive Recursive Functions 45
1-4.2 Partial Recursive Functions 50
1-5 TURING MACHINES AS ALGORITHMS 53
1-5.1 Solvability of Classes of Yes/No Problems 54
1-5.2 The Halting Problem of Turing Machines 56
1-5.3 The Word Problem ofSemi-Thue Systems 58
1-5.4 Post Correspondence Problem 60
1-5.5 Partial Solvability of Classes of Yes/No Problems 64
BIBLIOGRAPHIC REMARKS 67
REFERENCES 68
PROBLEMS 70
CHAPTER 2 PREDICATE CALCULUS
INTRODUCTION 77
2-1 BASIC NOTIONS 81
2-1.1 Syntax 81
2-1.2 Semantics (Interpretations) 85
2-1.3 Valid W ffs 90
2-1.4 Equivalence of Wffs 95
2-1.5 Normal Forms ofWffs 101
2-1.6 The Validity Problem 105
2-2 NATURAL DEDUCTION 108
2-2.1 Rules for the Connectives 110
2-2.2 Rules for the Quantifiers 115
2-2.3 Rules for the Operators 122
2-3 THE RESOLUTION METHOD 125
2-3.1 Clause Form 125
2-3.2 Herbrand's Procedures 130
2-3.3 The Unification Algorithm 136
2-3.4 The Resolution Rule 140
BIBLIOGRAPHIC REMARKS 145
REFERENCES 146
PROBLEMS 147
CHAPTER 3 VERIFICATION OF PROGRAMS 161
INTRODUCTION 161
3-1 FLOWCHART PROGRAMS 161
3-1.1 Partial Correctness 170
3-1.2 Termination 182
3-2 FLOWCHART PROGRAMS WITH ARRAYS 189
3-2.1 Partial Correctness 189
3-2.2 Termination 195
3-3 ALGOL-LIKE PROGRAMS 202
3-3.1 While Programs 203
3-3.2 Partial Correctness 205
3-3.3 Total Correctness 211
BIBLIOGRAPHIC REMARKS 218
REFERENCES 220
PROBLEMS 223
CHAPTER 4 FLOWCHART SCHEMAS 241
INTRODUCTION 241
4-1 BASIC NOTIONS 242
4-1.1 Syntax 242
4-1.2 Semantics (Interpretations) 244
4-1.3 Basic Properties 248
4-1.4 Herbrand Interpretations 260
4-2 DECISION PROBLEMS 262
4-2.1 Unsolvability of the Basic Properties 264
4-2.2 Free Schemas 268
4-2.3 Tree Schemas 274
4-2.4 Ianov Schemas 284
4-3 FORMALIZATION IN PREDICATE CALCULUS 294
4-3.1 The Algorithm 295
4-3.2 Formalization of Properties of Flowchart Programs 307
4-3.3 Formalization of Properties of Flowchart Schemas 311
4-4 TRANSLATION PROBLEMS 317
4-4.1 Recursive Schemas 319
4-4.2 Flowchart Schemas versus Recursive Schemas 322
BIBLIOGRAPHIC REMARKS 334
REFERENCES 335
PROBLEMS 337
CHAPTER 5 THE FIXPOINT THEORY OF PROGRAMS 356
INTRODUCTION 356
5-1 FUNCTIONS AND FUNCTIONALS 357
5-1.1 Monotonic Functions 359
5-1.2 Continuous Functionals 366
5-1.3 Fixpoints of Functionals 369
5-2 RECURSIVE PROGRAMS 374
5-2.1 Computation Rules 375
5-2.2 Fixpoint Computation Rules 384
5-2.3 Systems of Recursive Definitions 389
5-3 VERIFICA TION METHODS 392
5-3.1 Stepwise Computational Induction 393
5-3.2 Complete Computational Induction 400
5-3.3 Fixpoint Induction 403
5-3.4 Structural Induction 408
BIBLIOGRAPHIC REMARKS 415
REFERENCES 416
PROBLEMS 418
NAME INDEX
SUBJECT INDEX
· · · · · · (收起)