Non-standard algorithmic and dynamic logic. (English) Zbl 0594.68032
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 H. Andréka, I. Nemeti and 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 R. M. Burstall [Inform. Processing 74, Proc. IFIP Congr. 74, Stockholm, 308-312 (1974; Zbl 0299.68012)], C. A. R. Hoare [Commun. ACM 12, 576-580 (1969; Zbl 0179.231)], and 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 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 [R. W. Floyd, Proc. Symp. Appl. Math. 19, 19-32 (1967; Zbl 0189.502); C. A. R. Hoare, loc. cit.], R. M. Burstall’s modal logic [loc. cit.], A. Pnueli’s temporal logic for proving programs partially correct, the Manna-Cooper-method [Z. Manna, loc. cit.] for proving programs totally correct and 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.
The shortcomings with respect to the completeness and decidability of the proof concepts conceived by R. M. Burstall [Inform. Processing 74, Proc. IFIP Congr. 74, Stockholm, 308-312 (1974; Zbl 0299.68012)], C. A. R. Hoare [Commun. ACM 12, 576-580 (1969; Zbl 0179.231)], and 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 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 [R. W. Floyd, Proc. Symp. Appl. Math. 19, 19-32 (1967; Zbl 0189.502); C. A. R. Hoare, loc. cit.], R. M. Burstall’s modal logic [loc. cit.], A. Pnueli’s temporal logic for proving programs partially correct, the Manna-Cooper-method [Z. Manna, loc. cit.] for proving programs totally correct and 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.
Reviewer: R.Horsch
MSC:
| 68Q65 | Abstract data types; algebraic specification |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68-02 | Research exposition (monographs, survey articles) pertaining to computer science |
| 03B45 | Modal logic (including the logic of norms) |
| 03H99 | Nonstandard models |
Keywords:
formal program; verification methods; survey; partial and total correctness of programs; non-standard dynamic logicCitations:
Zbl 0475.68009; Zbl 0475.68010; Zbl 0299.68012; Zbl 0179.231; Zbl 0353.68066; Zbl 0039.008; Zbl 0189.502; Zbl 0403.03024References:
| [1] | Andréka, H.; Nemeti, I., Completeness of Floyd logic, Btdl. of the Section of Logic, Wrockzw (Lodz), 7, 115-120 (1978) · Zbl 0407.03034 |
| [2] | Andréka, H.; Nemeti, I.; Sain, I., Completeness problems in verification of programs and program schemes, MFCS ’79, Sprhlger Lec. Notes Comp. Sci, 74, 208-218 (1979) · Zbl 0411.03017 |
| [3] | Andréka, H.; Nemeti, I.; Sain, I., Henkin-type semantics for program schemes to turn negative results to positive, (FCT 79 (1979), Akademie Verlag: Akademie Verlag Berlin), 18-24 · Zbl 0418.03028 |
| [4] | Andréka, H.; Nemeti, I.; Sain, I., Program verification within and without logic, Bull. of Section of Logic, Wroclaw (Lodz), 8/3, 124-130 (1979) · Zbl 0441.68024 |
| [5] | Andréka, H.; Nemeti, I.; Sain, I., A characterization of Floyd provable program, MFCS ’81, Springer Lee. Notes Comp. Sei, 118, 162-171 (1981) · Zbl 0481.68035 |
| [6] | Andréka, H.; Nemeti, I.; Sain, I., A complete logic for reasoning about programs via nonstandard model theory, Parts I and II. Theor. Comp. Sci., 17, 193-212, 259-278 (1982) · Zbl 0475.68010 |
| [7] | Andréka, H., Sharpening the characterization of the power of Floyd’s method; logics of programs and their applications (A, Salwicki, ed.). SprhTger Lee. Notes Comp. Sci, 148, 1-26 (1983) · Zbl 0528.68007 |
| [8] | Apt, K. R., Ten years of Hoare’s logic: a survey-Part 1, ACM Trans. Prog. Lang. Syst, 3, 431-483 (1981) · Zbl 0471.68006 |
| [9] | Berman, F., A completeness technique for D-axiomatizable semantics, Proc. 11th ACM Syrup. Proc. 11th ACM Syrup, Theory of Compttt, 160-166 (1979) |
| [10] | Berman, F., Syntactic and semantic structure in propositional dynamic logic, Technical Report 79-07-05, 98-195 (1979), Dept. Comp. Sci., University of Washington, Seattle |
| [11] | Berman, F., Nonstandard models in propositional dynamic logic; Logics of programs and their applications (A, Salwicki, ed.). SprPtger Lec. Notes Comp. Sci, 148, 81-85 (1983) · Zbl 0523.03024 |
| [12] | Biro, B., On the completeness of program verification methods, Bull. of Section of Logic, Wroctaw (Lodz), 10, 83-90 (1981) · Zbl 0481.68034 |
| [13] | Biro, B.; Sain, I., Peano arithmetic for the time scale of nonstandard time models (1983), (Manuscript) |
| [14] | BurstalI, R. M., Program proving as hand simulation with a little induction, (Information Processing, 74 (1974), North-Holland: North-Holland Amsterdam), 308-312 · Zbl 0299.68012 |
| [15] | McCarthy, J.; Hayes, P. J., Some philosophical problems from the standpoint of artificial intelligence, (Meltzer; Michie, Machine Intelligence, 4 (1969), Edinburgh University Press: Edinburgh University Press Edinburgh), 463-502 · Zbl 0226.68044 |
| [16] | Cartwright, R., Nonstandard fixed points; Proc, Logics of Programs Workshop. CMU. Sprfnger Lec. Notes Comp. Sci, 164, 86-100 (1983) · Zbl 0566.68015 |
| [17] | Cartwright, R.; McCarthy, J., Recursive programs as functions in a first order theory (1979), Preprint Stanford Univ · Zbl 0407.68042 |
| [18] | Cook, S. A., Soundness and completeness of an axiom system for program verification, SlAM J. Comp, 7, 70-90 (1978) · Zbl 0374.68009 |
| [19] | Csirmaz, L., A survey of the semantics of Floyd-Hoare derivability, CL & CL, 14, 21-42 (1980) · Zbl 0466.68016 |
| [20] | Csirmaz, L., Structure of program runs of nonstandard time, Acta Cybernetica, 4, 325-331 (1980) · Zbl 0441.68026 |
| [21] | Csirmaz, L., Programs and program verifications in a general setting, Tlteor. Comp. Sci, 16, 199-211 (1981) · Zbl 0481.68016 |
| [22] | Csirmaz, L., On the strength of “sometimes” and “always” in program verification, Inf. Control, 57, 165-179 (1983) · Zbl 0549.68019 |
| [23] | Csinnaz, L., A completeness theorem for dynamic logic (1983), Notre Dame Journal of Formal Logic |
| [24] | Csirmaz, L.; Paris, J., A property of 2-sorted Peano models and program verification, Preprint Math. Inst. Hungar. Acad. Sci. (1981), to appear in Z. Math. Log & Grundl. Math. · Zbl 0564.03049 |
| [25] | Floyd, R. W., Assigning meanings to programs, (Providence, R. I., Proc. AMS Syrup. Proc. AMS Syrup, Applied Math, 19 (1967), American Math. Society), 19-31 · Zbl 0189.50204 |
| [26] | Gergely, T.; Szöts, M., On the incompleteness of proving partial correctness, Acta Cybernetica, 3, 45-57 (1979) · Zbl 0392.68010 |
| [27] | Gergeley, T.; Ury, L., Program behaviour specification through explicit time consideration, (Information Processing ”80 (1980), North-Holland: North-Holland Amsterdam), 107-111 · Zbl 0443.68007 |
| [28] | Gergely, T.; Ury, L., Time model for programming logic, (Bolyai, J., Math. Logic in Comp. Sci., Colloqu. Math. Soc., 26 (1981), North-Holland: North-Holland Amsterdam), 561-606 · Zbl 0496.68010 |
| [29] | Hajek, P., Making dynamic logic first order, MFCS. Sprbtger Lee. Notes Comp. Sci, 118, 287-295 (1981) · Zbl 0465.68010 |
| [30] | Hajek, P., Arithmetical interpretation of dynamic logic, J. Symbolie Logic, 48, 704-713 (1983) · Zbl 0546.03012 |
| [31] | Hajek, P., A simple dynamic predicate logic, Theor. Comp. Sci. (1983), (in press) |
| [32] | Hajek, P., Proc. Conf Algebra, Combinatorics and Logies in Com. Sci., Gyür, 1983. Proc. Conf Algebra, Combinatorics and Logies in Com. Sci., Gyür, 1983, Some conservativeness results in NDL (1983) |
| [33] | Harel, D.; Meyer, A. R.; Pratt, V. R., Computability and completeness in logics of programs, Proc. 9th ACM Syrup. Proc. 9th ACM Syrup, Theory of Comput., 261-268 (1977) |
| [34] | Harel, D., First-order dynamic logic, Springer Lec. Nates Comp. Sci., 68 (1979) · Zbl 0403.03024 |
| [35] | Henkin, L., Completeness in the theory of types, J, Symbolte Logic, 15, 81-91 (1950) · Zbl 0039.00801 |
| [36] | Hoare, C. A.R., An axiomatic basis for computer programming, Commun. ACM., 12, 576-580 (1969), 583 · Zbl 0179.23105 |
| [37] | Kfoury, D. J.; Park, D. M.R., On the termination of program schemes, hr, Control, 28, 251-293 (1975) · Zbl 0329.68015 |
| [38] | Manders, K. L.; Daley, R. F., The complexity of the validity problem for dynamic logic, Manuscript (1982), Univ. of Pittsburgh: Univ. of Pittsburgh PA · Zbl 0521.03023 |
| [39] | Manna, Z., Mathematieal Theory of Computation (1974), McGraw-Hill: McGraw-Hill New York · Zbl 0353.68066 |
| [40] | Manna, Z.; Pnueli, A., The modal logic of programs (1981), Preprint CS81-12 |
| [41] | Manna, Z.; Waldinger, R., Is “sometime” sometimes better than ’always’: Intermittent assertions in proving program correctness, Commun ACM, 21, 2, 159-172 (1978) · Zbl 0367.68011 |
| [42] | Mirkowska, G., On formalized systems of algorithmic logic, Bull. Aead. Palon. Sei., Ser. Sci. Math. Astron. Phys, 19, 421-428 (1971) · Zbl 0222.02010 |
| [43] | Naur, P., Proof of algorithms by general snapshots, BIT, 6, 310-316 (1966) |
| [44] | Nemeti, I., Nonstandard dynamic logic; Logics of programs (D, Kozen, ed.). Springer Lee. Notes Comp. Sci, 131, 311-348 (1982) · Zbl 0493.68032 |
| [45] | Nemeti, I., Nonstandard runs of Floyd-provable programs; Logics of programs and their applications (A, Salwicki, ed.). Springer Lee. Notes Comp. Sol, 148, 186-204 (1983) · Zbl 0519.68014 |
| [46] | Paris, J., Some independence results for Peano arithmetic, J. Symbolic Logic, 43, 725-731 (1978) · Zbl 0408.03048 |
| [47] | Pnueli, A., The temporal logic of programs, Proc. 18th EEE Syrup. Found. Proc. 18th EEE Syrup. Found, Comput. Sci., 46-57 (1977) |
| [48] | Pnueli, A., The temporal semantics of concurrent programs, Theor. Comp. Sci, 13, 45-60 (1981) · Zbl 0441.68010 |
| [49] | Pratt, V. R., Semantical considerations on Floyd-Hoare logic, Proc. 17th IEEE Syrup. Found. Proc. 17th IEEE Syrup. Found, Comput. Sci., 109-121 (1976) |
| [50] | Richter, M. M.; Szabo, M. E., Nonstandard computation theory, Proc. Conf. Algebra. Proc. Conf. Algebra, Combinatories and Logic in Comp. Sci., Györ. (1983) · Zbl 0507.03030 |
| [51] | Richter, M. M.; Szabo, M. E., Towards a nonstandard analysis of programs; Nonstandard analysis-recent developments (A, E. Hurd, ed.). Springer Lec. Notes Math, 983, 186-203 (1983) · Zbl 0507.03030 |
| [52] | Sain, I., First order dynamic logic with decidable proofs and workable model theory, In FCT ’81. Springer Lec. Notes Comp. Sci, 117, 334-340 (1981) · Zbl 0494.03022 |
| [53] | Sain, I., Total correctness in nonstandard dynamic logic, Theor. Comp. Sci. (1983), (in press) · Zbl 0538.68017 |
| [54] | Sain, I., A simple proof for the completeness of the Floyd method, Theor. Comp. Sci. (1983), (in press) |
| [55] | Sain, I., Structured nonstandard dynamic logic, Z. Math. Logik Grundl Math. (1983), to appear · Zbl 0552.68034 |
| [56] | Sain, I., Explicit characterization of the power of the Burstall-Pnueli-Manna temporal program verification method (1983), Mathematical Institute, Hungarian Academy of Sciences, preprint |
| [57] | Sain, I., Total correctness in nonstandard dynamic logic (1983), Mathematical Institute, Hungarian Academy of Sciences, preprint. · Zbl 0538.68017 |
| [58] | Sain, I., Successor axioms for time increase the program verification power of full computational induction (1983), Ann. Pure App. Logic (in press). |
| [59] | Salwicki, A., Formalized algorithmic languages, Bull. Aead. Polon. Sci., Ser. Sei. Math. Astron. Phys, 18, 227-232 (1970) · Zbl 0198.02801 |
| [60] | Tiuryn, J., A survey of the logic of effective definitions; Proc, workshop on logics of programs (E. Engeler, ed.). Springer Lee. Notes Comp. Sci, 125, 198-245 (1981) · Zbl 0468.68037 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
