Computability and completeness in logics of programs (Preliminary Report)

ABSTRACT

Dynamic logic is a generalization of first order logic in which quantifiers of the form “for all &khgr;...” are replaced by phrases of the form “after executing program &agr;...”. This logic subsumes most existing first-order logics of programs that manipulate their environment, including Floyd's and Hoare's logics of partial correctness and Manna and Waldinger's logic of total correctness, yet is more closely related to classical first-order logic than any other proposed logic of programs. We consider two issues: how hard is the validity problem for the formulae of dynamic logic, and how might one axiomatize dynamic logic? We give bounds on the validity problem for some special cases, including a &Pgr;02-completeness result for the partial correctness theories of uninterpreted flowchart programs. We also demonstrate the completeness of an axiomatization of dynamic logic relative to arithmetic.

REFERENCES

• 1: de Bakker, J.W., and W.P. de Roever. A calculus for recursive program schemes, in Automata, Languages and Programming (ed. Nivat), 167-196. North Holland, 1972.
• 2: Basu, S. K. and R. T. Yeh. Strong Verification of Programs. IEEE Trans. Software Engineering, SE-1, 3, 339-345.Sept. 75.
• 3: Burstall, R.M. Program Proving as Hand Simulation with a Little Induction. IFIP 1974, Stockholm.
• 4: Cook, S.A. Axiomatic and Interpretive Semantics for an Algol Fragment. TR-79, Toronto, Feb. 1975.
• 5: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 6: David Harel , Amir Puneli , Jonathan Stavi, A complete axiomatic system for proving deductions about recursive programs, Proceedings of the ninth annual ACM symposium on Theory of computing, p.249-260, May 04-04, 1977, Boulder, Colorado, United States [doi>10.1145/800105.803415]
• 7: Hitchcock, P. and D. Park. Induction Rules and Termination Proofs. In Automata, Languages and Programming (ed. Nivat, M.), IRIA. North-Holland, 1973.
• 8: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 9: Hughes, C.E. and M.J. Cresswell. An Introduction to Modal Logic. London: Methuen and Co Ltd. 1972.
• 10: Kripke, S. Semantical considerations on Modal Logic. Acta Philosophica Fennica, 83-94, 1963.
• 11: Luckham, D., D. Park and M. Paterson. On Formalized Computer Programs. J.CSS 3, 2, 119-127. May 1970.
• 12: Zohar Manna , Richard Waldinger, Is “sometime” sometimes better than “always”?: Intermittent assertions in proving program correctness, Proceedings of the 2nd international conference on Software engineering, p.32-39, October 13-15, 1976, San Francisco, California, United States
• 13: Pratt, V.R. Semantical Considerations on Floyd-Hoare Logic. 17th IEEE Symposium on Foundations of Computer Science, Oct. 1976.
• 14: Hartley Rogers, Jr., Theory of recursive functions and effective computability, MIT Press, Cambridge, MA, 1987
• 15: Tarski, A. The semantic conception of truth and the foundations of semantics. Philos. and Phenom. Res, 4, 341-376, 1944.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Computational logic

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.3 Complexity Measures and Classes
          Subjects: Reducibility and completeness
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Assertions
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Recursive function theory

General Terms:
Performance, Theory, Verification