In his paper “Ten thousend and one logics of programs” [MIT/LCS/TM-150 (1980)], A. R. Meyer mentions (only!) the following six program logics: E. Engeler’s (1967) and A. Salwicki’s (1970) algorithmic logic, A. Pnueli’s temporal logic (1977), V. R. Pratt’s dynamic logic (1978), R. Constable’s assertion language (1978), J. Tiuryn’s logic of effective definitions. All these logics are equivalent to various fragments of the (E. Engeler’s) logical language \(L_{\omega_ 1\omega}\) (an infinitary extension of the first-order language). They are, essentially, equivalent in expressive power, degree of undecidability, axiomatizability etc., and (can) represent (different or equivalent) types of (Kripke) modal logics of programs. Their propositional variants are a rich and powerful field of results on algebraic and logic models of programming.
The present book has its origin in A. Salwicki’s seminal paper “Formalized algorithmic languages” [Bull. Acad. Pol. Sci., Sér. Sci. Math. Astron. Phys. 18, 227-232 (1970; Zbl 0198.028)], proposing a whole research program, and in G. Mirkowska’s axiomatization (and completeness) results (1971) on algorithmic logic (AL). Chapter 2 presents the (logic) language of deterministic iterative programs. A formal (Hilbert-style) axiom system for AL, using \(\omega\)-types of inference rules, is proposed. Chapter 3 proves the AL completeness theorem and Gentzen-style AL axiomatization. Chapter 4 is dealing with the algorithmic properties of data structures: dictionary, queue, and stack theories, arrays, hash tables, implementations in the LOGLAN programming language project of the Warsaw University. Chapter 5 is devoted to propositional AL with important algebraic counterparts. Chapter 6 extends the AL language towards non-determinism. A complete (but infinitary) Hilbert-style axiomatization is provided. Chapter 7 presents a method for formal specification of the LOGLAN language, and its model of concurrent computations, called MAX. Within the LOGLAN project, the authors and their collaborators create a family of algorithmic theories that will formally describe the different aspects of LOGLAN semantics. These theories are complementing and concatenating each other (and together) for the different modules of a program.
This book is a significant advance in the field of algorithmic languages, modelling imperative programming languages, the various (sequential and parallel) control and data structures. AL constitutes also a uniform approach to Church’s thesis on effective computability and programmability, on the theory of algorithms and their computational complexity. The present approach proves to be a real step forward concerning the program behaviour philosophy, against arbitrariness and falsity in this field. It comes from a well-known school of (mathematical and logical) original thinking: the Polish one!