Mirkowska G., Salwicki A. Algorithmic Logic

D. Reidel, 1987. — 384 p.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.The motivations
An informal introduction to formalized languages
Assigning meanings to programs
Semantic properties of programs
Expressivity. An introduction to the language of algorithmic logic
On applications
Logic of deterministic iterative programs
Language
Semantics
Expressiveness
Properties of the semantic consequence operation
Axiomatization
Models and consistency
Useful tautologies and inference rules
An example of a correctness proofMetamathematical investigations of algorithmic logic
Lindenbaum algebra
The Completeness Theorem
Two corollaries of the Completeness Theorem
The standard execution method is implicitly defined by the axiomatization of algorithmic logic
Gentzen type axiomatization
The normal form of programs
Equality
Generalized terms
ial functions
Many sorted structures
Definability and programmability
Inessentiality of definitionsAlgorithmic properties of data structures
Data structures in programming
Dictionaries
Theory of dictionaries
Representation theorem for models of ATD
On complexity of ATD
The theory of priority queues
The theory of natural numbers
Stacks
The theory of stacks
The representation theorem for stacks
Implementation of arithmetic and dictionaries
Theory of links and stacks — ATSL
Implementation of stacks in LOGLAN programming language
Queues
Binary trees
Binary search trees
An interpretation of the theory of priority queues
An implementation of priority queues
Arrays
Hashtables
Rational numbers
Complex numbers
Real numbers
Concluding remarksPropositional algorithmic logic
Syntax and semantics
Semantic properties of program schemes
Properties of semantic structures
The semantic consequence operation is not compact
The syntactic consequence operation
Examples of propositional theories
Lindenbaum algebra
Deterministic and total interpretations of atomic programs
ial functional interpretations
Bounded non-determinism: The Completeness Theorem
Elimination of bounded non-deterministic program variables
Yanov schemes
Application of PAL in microprogrammingNon-determinism in algorithmic logic
Non-deterministic while-programs and their semantics
Properties of non-deterministic programs
The Substitution Theorem
Non-deterministic algorithmic logic
Certain metamathematical results
On isomorphism of data structures
On the equivalence of non-deterministic programsProblems and theories inspired by the LOGLAN project
Concurrent programs
MAX semantics
Comparison with some other concepts of concurrency
A comparison of MAX and ARB semantics in the case of Petri nets
Critical remarks concerning MAX semantics
LIBERAL semantics
An algorithmic theory of references
Representation theorem for ATR theory
Specification of univocal references
Virtual memory
Concatenable type declarations
An implementation of rational numbers(Scanned by Envoy)