The purpose of this book is manyfold. It is intended both to present techniques useful in software engineering and to expose results of research on properties of these techniques.
The major goal of the book is to help the reader in elaboration of his own views on foundations of computing. The present authors believe that semantics of programs will always be the necessary foundation for every student of computing. On this foundation one can construct subsequent layers of skill and knowledge in computer science. Later one discovers more questions of a different nature, e.g. on cost and optimality of algorithms. This book shall be mainly concerned with semantics.
Secondly, the book aims to supply a new set of logical axioms and inference rules appropriate for reasoning about the properties of algorithms. Such tools are useful for formalizing the verification and analysis of algorithms. The tools should be of quality — they should be consistent and complete. These and similar requirements lead us toward metamathematical questions concerning the structure of algorithmic logic.
Author(s): Grazyna Mirkowska, Andrzej Salwicki
Publisher: D. Reidel
Year: 1987
Language: English
Commentary: Scanned, DjVu'ed, OCR'ed, TOC by Envoy
Pages: 384
Cover ......Page 1
Table of contents ......Page 4
Preface ......Page 8
1. The motivations ......Page 11
2. An informal introduction to formalized languages ......Page 15
3. Assigning meanings to programs ......Page 21
4. Semantic properties of programs ......Page 26
5. Expressivity. An introduction to the language of algorithmic logic ......Page 28
6. On applications ......Page 30
Chapter II. Logic of deterministic iterative programs ......Page 33
1. Language ......Page 34
2. Semantics ......Page 40
3. Expressiveness ......Page 48
4. Properties of the semantic consequence operation ......Page 61
5. Axiomatization ......Page 66
6. Models and consistency ......Page 75
7. Useful tautologies and inference rules ......Page 79
8. An example of a correctness proof ......Page 85
Bibliographic remarks ......Page 87
1. Lindenbaum algebra ......Page 89
2. The Completeness Theorem ......Page 99
3. Two corollaries of the Completeness Theorem ......Page 105
4. The standard execution method is implicitly defined by the axiomatization of algorithmic logic ......Page 107
5. Gentzen type axiomatization ......Page 113
6. The normal form of programs ......Page 119
7. Equality ......Page 125
8. Generalized terms ......Page 129
9. Partial functions ......Page 132
10. Many sorted structures ......Page 137
11. Definability and programmability ......Page 141
12. Inessentiality of definitions ......Page 145
Bibliographic remarks ......Page 147
1. Data structures in programming ......Page 148
2. Dictionaries ......Page 151
3. Theory of dictionaries ......Page 152
4. Representation theorem for models of ATD ......Page 159
5. On complexity of ATD ......Page 161
6. The theory of priority queues ......Page 164
7. The theory of natural numbers ......Page 165
8. Stacks ......Page 169
9. The theory of stacks ......Page 170
10. The representation theorem for stacks ......Page 174
11. Implementation of arithmetic and dictionaries ......Page 176
12. Theory of links and stacks—ATSL ......Page 177
13. Implementation of stacks in LOGLAN programming language ......Page 183
14. Queues ......Page 186
15. Binary trees ......Page 189
16. Binary search trees ......Page 191
17. An interpretation of the theory of priority queues ......Page 194
18. An implementation of priority queues ......Page 197
19. Arrays ......Page 200
20. Hashtables ......Page 203
21. Rational numbers ......Page 204
22. Complex numbers ......Page 205
23. Real numbers ......Page 210
24. Concluding remarks ......Page 212
Bibliographic remarks ......Page 214
Chapter V. Propositional algorithmic logic ......Page 216
1. Syntax and semantics ......Page 218
2. Semantic properties of program schemes ......Page 222
3. Properties of semantic structures ......Page 231
4. The semantic consequence operation is not compact ......Page 238
5. The syntactic consequence operation ......Page 239
6. Examples of propositional theories ......Page 243
7. Lindenbaum algebra ......Page 247
8. Deterministic and total interpretations of atomic programs ......Page 249
9. Partial functional interpretations ......Page 253
10. Bounded non-determinism: The Completeness Theorem ......Page 258
11. Elimination of bounded non-deterministic program variables ......Page 267
12. Yanov schemes ......Page 271
13. Application of PAL in microprogramming ......Page 273
Bibliographic remarks ......Page 278
Chapter VI. Non-determinism in algorithmic logic ......Page 279
1. Non-deterministic while-programs and their semantics ......Page 280
2. Properties of non-deterministic programs ......Page 283
3. The Substitution Theorem ......Page 287
4. Non-deterministic algorithmic logic ......Page 292
5. Certain metamathematical results ......Page 296
6. On isomorphism of data structures ......Page 299
7. On the equivalence of non-deterministic programs ......Page 301
Bibliographic remarks ......Page 307
Chapter VII. Problems and theories inspired by the LOGLAN project ......Page 308
1. Concurrent programs ......Page 309
2. MAX semantics ......Page 310
3. Comparison with some other concepts of concurrency ......Page 313
4. A comparison of MAX and ARB semantics in the case of Petri nets ......Page 321
5. Critical remarks concerning MAX semantics ......Page 325
6. LIBERAL semantics ......Page 328
7. An algorithmic theory of references ......Page 338
8. Representation theorem for ATR theory ......Page 342
9. Specification of univocal references ......Page 348
10. Virtual memory ......Page 349
11. Concatenable type declarations ......Page 351
12. An implementation of rational numbers ......Page 354
Bibliographic remarks ......Page 356
Appendix A. Boolean algebras ......Page 358
Appendix B. The proof of Lemma 2.2 from Chapter III ......Page 362
Bibliography ......Page 366
Index ......Page 379
Errata ......Page 383
Back cover ......Page 384
