Non-standard algorithmic and dynamic logic (Q1077159): Difference between revisions

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.