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 by Envoy
Pages: 384
City: Warszawa
CHAPTER I. INTRODUCTION 1
1. The motivations 1
2. An informal introduction to formalized languages 5
3. Assigning meanings to programs 11
4. Semantic properties of programs 16
5. Expressivity. An introduction to the language of algorithmic logic 18
6. On applications 20
CHAPTER II. LOGIC OF DETERMINISTIC ITERATIVE PROGRAMS 23
1. Language 24
2. Semantics 30
3. Expressiveness 38
4. Properties of the semantic consequence operation 51
5. Axiomatization 56
6. Models and consistency 65
7. Useful tautologies and inference rules 69
8. An example of a correctness proof 75
Bibliographic remarks 77
CHAPTER III. METAMATHEMATICAL INVESTIGATIONS
OF ALGORITHMIC LOGIC 79
1. Lindenbaum algebra 79
2. The Completeness Theorem 89
3. Two corollaries of the Completeness Theorem 95
4. The standard execution method is implicitly defined by the axiomatization of algorithmic logic 97
5. Gentzen type axiomatization 103
6. The normal form of programs 109
7. Equality 115
8. Generalized terms 119
9. Partial functions 122
10. Many sorted structures 127
11. Definability and programmability 131
12. Inessentiality of definitions 135
Bibliographic remarks 137
CHAPTER IV. ALGORITHMIC PROPERTIES OF DATA STRUCTURES 138
1. Data structures in programming 138
2. Dictionaries 141
3. Theory of dictionaries 142
4. Representation theorem for models of ATD 149
5. On complexity of ATD 151
6. The theory of priority queues 154
7. The theory of natural numbers 155
8. Stacks 159
9. The theory of stacks 160
10. The representation theorem for stacks 164
11. Implementation of arithmetic and dictionaries 166
12. Theory of links and stacks—ATSL 167
13. Implementation of stacks in LOGLAN programming language 173
14. Queues 176
35. Binary trees 179
16. Binary search trees 181
17. An interpretation of the theory of priority queues 184
18. An implementation of priority queues 187
19. Arrays 190
20. Hashtables 193
21. Rational numbers 194
22. Complex numbers 195
23. Real numbers 200
24. Concluding remarks 202
Bibliographic remarks 204
CHAPTER V. PROPOSITIONAL ALGORITHMIC LOGIC 206
1. Syntax and semantics 208
2. Semantic properties of program schemes 212
3. Properties of semantic structures 221
4. The semantic consequence operation is not compact 228
5. The syntactic consequence operation 229
6. Examples of propositional theories 233
7. Lindenbaum algebra 237
8. Deterministic and total interpretations of atomic programs 239
9. Partial functional interpretations 243
10. Bounded non-determinism: The Completeness Theorem 248
11. Elimination of bounded non-deterministic program variables 257
12. Yanov schemes 261
13. Application of PAL in microprogramming 263
Bibliographic remarks 268
CHAPTER VI. NON-DETERMINISM IN ALGORITHMIC LOGIC 269
1. Non-deterministic while-programs and their semantics 270
2. Properties of non-deterministic programs 273
3. The Substitution Theorem 277
4. Non-deterministic algorithmic logic 282
5. Certain metamathematical results 286
6. On isomorphism of data structures 289
7. On the equivalence of non-deterministic programs 291
Bibliographic remarks 297
CHAPTER VII. PROBLEMS AND THEORIES INSPIRED BY THE LOGLAN PROJECT 298
1. Concurrent programs 299
2. MAX semantics 300
3. Comparison with some other concepts of concurrency 303
4. A comparison of MAX and ARB semantics in the case
of Petri nets 311
5. Critical remarks concerning MAX semantics 315
6. LIBERAL semantics 318
7. An algorithmic theory of references 328
8. Representation theorem for ATR theory 332
9. Specification of univocal references 338
10. Virtual memory 339
11. Concatenable type declarations 341
12. An implementation of rational numbers 344
Bibliographic remarks 346
Appendix A. Boolean algebras 348
Appendix B. The proof of Lemma 2.2 from Chapter III 352
Bibliography 356
