With the objective of making into a science the art of verifying computer programs (debugging), the author addresses both practical and theoretical aspects. Subjects include computability (with discussions of finite automata and Turing machines); predicate calculus; verification of programs (bloth flowchart and algol-like programs); flowchart schemas; and the fixpoint theory of programs. 1974 edition. Includes 77 figures.
Author(s): Zohar Manna
Series: Mcgraw-Hill Computer Science Series
Publisher: Mcgraw-Hill College
Year: 1974
Language: English
Pages: 459
Cover......Page __sk_0000.djvu
Copyright......Page __sk_0002.djvu
Contents......Page __sk_0003.djvu
Preface......Page __sk_0007.djvu
Introduction......Page __sk_0011.djvu
1-1 Finite Automata......Page __sk_0012.djvu
1-1.1 Regular Expressions......Page __sk_0013.djvu
1-1.2 Finite Automata......Page __sk_0017.djvu
1-1.3 Transition Graphs......Page __sk_0019.djvu
1-1.4 Kleene's Theorem......Page __sk_0021.djvu
1-1.5 The Equivalence Theorem......Page __sk_0027.djvu
1-2 Turing Machines......Page __sk_0030.djvu
1-2.1 Turing Machines......Page __sk_0031.djvu
1-2.2 Post Machines......Page __sk_0034.djvu
1-2.3 Finite Machines with Pushdown Stores......Page __sk_0039.djvu
1-2.4 Nondeterminism......Page __sk_0045.djvu
1-3 Turing Machines as Acceptors......Page __sk_0047.djvu
1-3.1 Recursively Enumerable Sets......Page __sk_0048.djvu
1-3.2 Recursive Sets......Page __sk_0049.djvu
1-3.3 Formal Languages......Page __sk_0051.djvu
1-4 Turing Machines as Generators......Page __sk_0053.djvu
1-4.1 Primitive Recursive Functions......Page __sk_0055.djvu
1-4.2 Partial Recursive Functions......Page __sk_0060.djvu
1-5 Turing Machines as Algorithms......Page __sk_0063.djvu
1-5.1 Solvability of Classes of Yes/No Problems......Page __sk_0064.djvu
1-5.2 The Halting Problem of Turing Machines......Page __sk_0066.djvu
1-5.3 The Word Problem ofSemi-Thue Systems......Page __sk_0068.djvu
1-5.4 Post Correspondence Problem......Page __sk_0070.djvu
1-5.5 Partial Solvability of Classes of Yes/No Problems......Page __sk_0074.djvu
Bibliographic Remarks......Page __sk_0077.djvu
References......Page __sk_0078.djvu
Problems......Page __sk_0080.djvu
Introduction......Page __sk_0087.djvu
2-1.1 Syntax......Page __sk_0091.djvu
2-1.2 Semantics (Interpretations)......Page __sk_0095.djvu
2-1.3 Valid Wffs......Page __sk_0100.djvu
2-1.4 Equivalence of Wffs......Page __sk_0105.djvu
2-1.5 Normal Forms of Wffs......Page __sk_0111.djvu
2-1.6 The Validity Problem......Page __sk_0115.djvu
2-2 Natural Deduction......Page __sk_0118.djvu
2-2.1 Rules for the Connectives......Page __sk_0120.djvu
2-2.2 Rules for the Quantifiers......Page __sk_0125.djvu
2-2.3 Rules for the Operators......Page __sk_0132.djvu
2-3.1 Clause Form......Page __sk_0135.djvu
2-3.2 Herbrand's Procedures......Page __sk_0140.djvu
2-3.3 The Unification Algorithm......Page __sk_0146.djvu
2-3.4 The Resolution Rule......Page __sk_0150.djvu
Bibliographic Remarks......Page __sk_0155.djvu
References......Page __sk_0156.djvu
Problems......Page __sk_0157.djvu
3-1 Flowchart Programs......Page __sk_0171.djvu
3-1.1 Partial Correctness......Page __sk_0180.djvu
3-1.2 Termination......Page __sk_0192.djvu
3-2.1 Partial Correctness......Page __sk_0199.djvu
3-2.2 Termination......Page __sk_0205.djvu
3-3 Algol-like Programs......Page __sk_0212.djvu
3-3.1 While Programs......Page __sk_0213.djvu
3-3.2 Partial Correctness......Page __sk_0215.djvu
3-3.3 Total Correctness......Page __sk_0221.djvu
Bibliographic Remarks......Page __sk_0228.djvu
References......Page __sk_0230.djvu
Problems......Page __sk_0233.djvu
Introduction......Page __sk_0251.djvu
4-1.1 Syntax......Page __sk_0252.djvu
4-1.2 Semantics (Interpretations)......Page __sk_0254.djvu
4-1.3 Basic Properties......Page __sk_0258.djvu
4-1.4 Herbrand Interpretations......Page __sk_0270.djvu
4-2 Decision Problems......Page __sk_0272.djvu
4-2.1 Unsolvability of the Basic Properties......Page __sk_0274.djvu
4-2.2 Free Schemas......Page __sk_0278.djvu
4-2.3 Tree Schemas......Page __sk_0284.djvu
4-2.4 Ianov Schemas......Page __sk_0294.djvu
4-3 Formalization in Predicate Calculus......Page __sk_0304.djvu
4-3.1 The Algorithm......Page __sk_0305.djvu
4-3.2 Formalization of Properties of Flowchart Programs......Page __sk_0317.djvu
4-3.3 Formalization of Properties of Flowchart Schemas......Page __sk_0321.djvu
4-4 Translation Problems......Page __sk_0327.djvu
4-4.1 Recursive Schemas......Page __sk_0329.djvu
4-4.2 Flowchart Schemas versus Recursive Schemas......Page __sk_0332.djvu
Bibliographic Remarks......Page __sk_0344.djvu
References......Page __sk_0345.djvu
Problems......Page __sk_0347.djvu
Introduction......Page __sk_0366.djvu
5-1 Functions And Functionals......Page __sk_0367.djvu
5-1.1 Monotonic Functions......Page __sk_0369.djvu
5-1.2 Continuous Functionals......Page __sk_0376.djvu
5-1.3 Fixpoints of Functionals......Page __sk_0379.djvu
5-2 Recursive Programs......Page __sk_0384.djvu
5-2.1 Computation Rules......Page __sk_0385.djvu
5-2.2 Fixpoint Computation Rules......Page __sk_0394.djvu
5-2.3 Systems of Recursive Definitions......Page __sk_0399.djvu
5-3 Verification Methods......Page __sk_0402.djvu
5-3.1 Stepwise Computational Induction......Page __sk_0403.djvu
5-3.2 Complete Computational Induction......Page __sk_0410.djvu
5-3.3 Fixpoint Induction......Page __sk_0413.djvu
5-3.4 Structural Induction......Page __sk_0418.djvu
Bibliographic Remarks......Page __sk_0425.djvu
References......Page __sk_0426.djvu
Problems......Page __sk_0428.djvu
Name Index......Page __sk_0443.djvu
Subject Index......Page __sk_0447.djvu
