The theory of computer science: A programming approach

Cover......Page __sk_0000.djvu
Copyright......Page __sk_0002.djvu
Contents......Page __sk_0005.djvu
Preface......Page __sk_0009.djvu
1.1 Introduction......Page __sk_0013.djvu
1.2.1 Defining \'computable\'......Page __sk_0015.djvu
1.2.3 The limitations of our intuition......Page __sk_0018.djvu
1.3 Part 2: Towards a theory of computer science......Page __sk_0020.djvu
1.3.1 Problem solving......Page __sk_0021.djvu
1.3.2 Programming languages......Page __sk_0022.djvu
1.3.3 Data structures......Page __sk_0024.djvu
1.3.5 Program termination......Page __sk_0025.djvu
1.3.7 Computers......Page __sk_0026.djvu
2.2 Basic machines and finite state machines......Page __sk_0031.djvu
2.3 Sequences of inputs; states......Page __sk_0036.djvu
2.4 The limitations of finite state machines......Page __sk_0040.djvu
2.5 Turing machines......Page __sk_0042.djvu
2.6 A universal Turing machine......Page __sk_0051.djvu
2.7 Shannon\'s complexity measure for Turing machines......Page __sk_0053.djvu
2.8 More computer-like abstract machines......Page __sk_0058.djvu
2.8.1 B machines......Page __sk_0059.djvu
2.8.2 Program machines......Page __sk_0060.djvu
2.8.3 RASP\'s......Page __sk_0062.djvu
3.1 Introduction......Page __sk_0063.djvu
3.2 A non-computable function......Page __sk_0065.djvu
3.3 Enumerability and decidability......Page __sk_0068.djvu
3.3.1 Enumerability......Page __sk_0069.djvu
3.3.2 Decidability......Page __sk_0076.djvu
3.4.1 Recursive function theory......Page __sk_0081.djvu
3.4.2 Computability results in mathematics and logic......Page __sk_0083.djvu
3.4.3 Program schemas: the work of Luckham, Park, and Paterson......Page __sk_0087.djvu
3.4.4 Formal language theory: the syntax of programming languages......Page __sk_0095.djvu
4.1 Introduction......Page __sk_0104.djvu
4.2 The general recursive functions......Page __sk_0108.djvu
4.2.1 Generalized composition......Page __sk_0109.djvu
4.2.2 Primitive recursion......Page __sk_0112.djvu
4.2.3 The GRF......Page __sk_0116.djvu
4.3.1 Ackermann\'s function......Page __sk_0121.djvu
5.2 A GRF simulator for Turing machines......Page __sk_0129.djvu
5.2.1 Initialize......Page __sk_0130.djvu
5.2.2 Mainloop......Page __sk_0131.djvu
5.2.3 Extractresult......Page __sk_0134.djvu
5.2.4 Ackermann\'s function is a GRF......Page __sk_0135.djvu
5.3 A Turing machine compiler for the GRF......Page __sk_0137.djvu
5.4 Numbers as data structures......Page __sk_0141.djvu
6.1 Introduction......Page __sk_0149.djvu
6.2 McCarthy\'s formalism......Page __sk_0151.djvu
6.3 S-expressions......Page __sk_0159.djvu
6.4 Application of the formalism: equivalence of programs......Page __sk_0166.djvu
6.5 Application of the formalism: the meaning of programming languages......Page __sk_0180.djvu
7.1 Introduction......Page __sk_0187.djvu
7.2 Program testing......Page __sk_0191.djvu
7.3.1 Introduction: Floyd\'s work......Page __sk_0198.djvu
7.3.2 Hoare\'s logic of programs......Page __sk_0209.djvu
7.3.3 Towards automatic proofs of correctness......Page __sk_0218.djvu
7.4.1 Introduction......Page __sk_0220.djvu
7.4.2 The correctness of flow chart programs......Page __sk_0221.djvu
7.5 Reflections......Page __sk_0226.djvu
8.1 Introduction......Page __sk_0230.djvu
8.2 The lambda calculus......Page __sk_0236.djvu
8.3.1 Observing the basic correspondence......Page __sk_0243.djvu
8.3.2 Evaluating AEs......Page __sk_0246.djvu
8.3.3 Translating ALGOL 60 into (imperative) AEs......Page __sk_0250.djvu
8.3.4 Postscript on operational semantics: VDL......Page __sk_0252.djvu
8.4 Mathematical semantics: de-emphasizing the machine......Page __sk_0253.djvu
Appendix A Mathematical Prerequisites......Page __sk_0265.djvu
Appendix B Programming Prerequisites......Page __sk_0280.djvu
References......Page __sk_0284.djvu
Author Index......Page __sk_0293.djvu
Subject Index......Page __sk_0295.djvu