Non-standard algorithmic and dynamic logic

Modal logic (including the logic of norms) (03B45) Nonstandard models (03H99) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Review text

This paper surveys the state of the art of formal methods for proving both partial and total correctness of programs focussing on non-standard dynamic logic established recently in the fundamental papers of \textit{H. Andréka}, \textit{I. Nemeti} and \textit{I. Sain} [Theor. Comput. Sci. 17, 193-212, 259-278 (1982; Zbl 0475.68009 and Zbl 0475.68010)]. The shortcomings with respect to the completeness and decidability of the proof concepts conceived by \textit{R. M. Burstall} [Inform. Processing 74, Proc. IFIP Congr. 74, Stockholm, 308-312 (1974; Zbl 0299.68012)], \textit{C. A. R. Hoare} [Commun. ACM 12, 576-580 (1969; Zbl 0179.231)], and \textit{Z. Manna} [Mathematical theory of computation (1974; Zbl 0353.68066)] are overcome by results of non-standard dynamic logic (NDL henceforth). NDL is a complete first order logic with decidable proof concept for reasoning about programs. The notion non-standard refers to non- standard model theory, devised by \textit{L. Henkin} [J. Symb. Logic 15, 81- 91 (1950; Zbl 0039.008)], to turn negative completeness results into positive ones, thus making proofs of non-provability feasible. Further on NDL is defined in algebraic terms. Based on the algebraic notions of NDL the most important results are compiled with special emphasis being directed to the characterization of program verification methods within NDL and corresponding completeness theorems, and to the comparison of reasoning power of program verification methods and deriving new methods from NDL. The Floyd-Hoare-method [\textit{R. W. Floyd}, Proc. Symp. Appl. Math. 19, 19-32 (1967; Zbl 0189.502); \textit{C. A. R. Hoare}, loc. cit.], \textit{R. M. Burstall}'s modal logic [loc. cit.], \textit{A. Pnueli}'s temporal logic for proving programs partially correct, the Manna-Cooper-method [\textit{Z. Manna}, loc. cit.] for proving programs totally correct and \textit{D. Harel}'s [First-order dynamic logic (1979; Zbl 0403.03024)] program verification method with respect to standard dynamic formulas are re- visited in view of NDL. The relationship between the reasoning powers of formal proof concepts is built up by lattice-theoretic terms with the notion of partial correctness as ordering relation and NDL being the appropriate model to build in. An elaborate bibliography offers ample opportunity to the interested reader to thoroughly study all known formal proof methods for program verification.

Recommendations

Cites work

Cited in

(20)

This page was built for publication: Non-standard algorithmic and dynamic logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1077159)