On the theory of programming logics

ABSTRACT

A new logic for reasoning about programs is proposed here, and its metamathematics is investigated. No new primitive notions are needed for the logic beyond those used in elementary programming and mathematics, yet the combination of these notions is remarkably powerful. The logic includes a programming language, designed with Michael O'Donnell, for program verification. It forms the core of the PL/CV verifier at Cornell. This study belongs to the discipline of Algorithmic Logic as conceived by Engeler. The logic is related to Park's mu-calculus based on functions instead of relations. The monadic quantifier free subset is developed in the style of the system in J.W. deBakker's Recursive Procedures. But this logic is substantially different from either of these. It is intended to be a practical programming logic in the spirit of E. Dijkstra's calculus. This paper proves the completeness and decidability of the monadic (iterative) programming logic. It discusses the polyadic logic and the programming language briefly, and considers general models for the iterative programming logic. The polyadic logic is shown to be incomplete with respect to standard models, but complete with respect to general models.

REFERENCES

• 1: Ashcroft, E.A. Program Verification Tableaus preprint 1975.
• 2: deBakker, J.W. and Scott, D. A Theory of Programs, Unpublished manuscript, 1969.
• 3: deBakker, J.W. Recursive Procedures, Mathematical Center, Amsterdam, 1971.
• 4: deBakker, J.W. and Meertens, L.G.L.T. On the Completeness of the Inductive Assertion Method, JCSS. 11. 3. December 1975, 323-357.
• 5: Cherniavsky, J.C. and Constable, R. L. "Representing Program Schemes in Logic". Proc. Of 13th Switching & Automata Theory Conf., October 1972, 27-39.
• 6: Church, A. Introduction to Mathematical Logic, Vol. I, Princeton Univ. Press 1956.
• 7: Edmund Melson Clarke, Jr., Completeness and incompleteness theorems for hoare-like axiom systems., 1976
• 8: Clint, M. and Hoare, C.A.R. Program Proving: Jumps and Functions, Acta Informatica 1, 1972.
• 9: Constable, R.L. Constructive Mathematics and Automatic Program Writers. Proceedings of IFIP Congress, Ljubljana, 1971, 229-233.
• 10: Robert L. Constable, Language Features that Support Program Verification (illustrated in PL/C), Cornell University, Ithaca, NY, 1976
• 11: Robert L. Constable , James E. Donahue, An Elementary Formal Semantics for the Programming Language PL/CS, Cornell University, Ithaca, NY, 1976
• 12: Constable, R.L. and O'Donnell, M.J. A Logic for Reasoning about Programs. Draft Monograph.
• 13: Cook, S.A. Axiomatic and Interpretive Semantics For An Algol Fragment. Tech. Rpt. 79, Comp. Sci. Dept., University of Toronto (to appear SICOMP).
• 14: Conway, R.W. and Constable, R.L. PL/CS - A Highly Disciplined Subset of PL/CS. Cornell Comp. Sci. Tech. Rpt. TR 76-273, 1976.
• 15: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 16: James Edward Donahue, Complementary Definitions of Programming Language Semantics, Springer-Verlag New York, Inc., Secaucus, NJ, 1976
• 17: Eilenberg, S. and Elgot, C. Recursiveness, Academic Press, New York, 1970.
• 18: Enderton, H.B. A Mathematical Introduction to Logic. Academic Press, New York, 1972.
• 19: Engeler, E. Formal Languages: Automata and Structures, Markham, 1968, 81pp.
• 20: Engeler, E. Structure and Meaning of Elementary Programs, Symposium on Semantics of Algorithmic Languages, Lecture Notes in Mathematics 188, Springer-Verlag, New York 1971, pp. 89-101.
• 21: Engeler, E. Algorithmic Logic, Foundations of Computer Science, ed. J.W. deBakker, Math. Centre Tracts, 63, Amsterdam, 1975, pp. 57-85.
• 22: Floyd, R.W. Assigning Meaning to Programs, Proceedings of Symposia in Applied Mathematics, Vol. XIX, American Math. Soc., 1967, pp. 19-32.
• 23: Friedman, E.P. Equivalence Problems in Monadic Recursion Schemes. Proc. 14th Annual Symposium on Switching and Automata Theory, Iowa City, IA 1973, pp. 26-33.
• 24: Garland, S.J. and Luckham, D.C. Program Schemes, Recursion Schemes and Formal Languages. JCSS, 7,2, April 1973, pp. 119-160.
• 25: Sheila A. Greibach, Theory of Program Structures: Schemes, Semantics, Verification, Springer-Verlag New York, Inc., Secaucus, NJ, 1985
• 26: Hitchcock, P. and Park, D. Induction Rules and Termination Proofs in Automata, Languages and Programs, ed. M. Nivat, North-Holland, 1972.
• 27: 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]
• 28: Hoare, C.A.R. Procedures and Parameters, An Axiomatic Approach , Symposium on Semantics of Algorithmic lanuguages, ed. E. Engeler, Springer-Verlag, Lecture Notes in Math. 188, 1971.
• 29: Hoare,C.A.R. and Wirth, N. An Axiomatic Definition of the Programming Language Pascal Acta Informatica 2, 1973, pp. 333-335.
• 30: Igarashi, S., London, R.L. and Luckham, D.C. Automatic Program Verification I: A Logical Basis and Its Implementation, Acta Informatica 4, 1975, pp. 145-182.
• 31: James C. King , Robert W. Floyd, An interpretation oriented theorem prover over integers, Proceedings of the second annual ACM symposium on Theory of computing, p.169-179, May 04-06, 1970, Northampton, Massachusetts, United States [doi>10.1145/800161.805162]
• 32: James C. King, Symbolic execution and program testing, Communications of the ACM, v.19 n.7, p.385-394, July 1976 [doi>10.1145/360248.360252]
• 33: Kleene, S.C. Introduction to Metamathematics, D. VanNostrand, Princeton, 1952, 550 pp.
• 34: Luckham, D.C., Park, M.R. and Paterson, M.S. On Formalized Computer Programs, JCSS, 4, 1970, pp. 220-249.
• 35: Manna, Z. The Correctness of Programs, JCSS, 3, 1969, pp. 119-127.
• 36: Zohar Manna , Jean Vuillemin, Fixpoint approach to the theory of computation, Communications of the ACM, v.15 n.7, p.528-536, July 1972 [doi>10.1145/361454.361460]
• 37: Zohar Manna, Introduction to Mathematical Theory of Computation, McGraw-Hill, Inc., New York, NY, 1974
• 38: Manna, Z. and Pneuli, A. Axiomatic Approach to Total Correctness of Programs, Acta Informatica, 3, 1974, pp. 243-263.
• 39: John McCarthy, Recursive functions of symbolic expressions and their computation by machine, Part I, Communications of the ACM, v.3 n.4, p.184-195, April 1960 [doi>10.1145/367177.367199]
• 40: Robin Milner, Implementation and applications of Scott's logic for computable functions, Proceedings of ACM conference on Proving assertions about programs, p.1-6, January 06-07, 1972, Las Cruces, New Mexico, United States
• 41: Park, D.M.R. Fixedpoint Induction and Proofs of Program Properties. Machine Intelligence 5, Edinburgh, 1969, pp. 59-78.
• 42: Pratt, V.R. Semantical Considerations on Floyd-Haore Logic. Proc. of 17th Annual Symp. on Foundations of Comp. Sci., Huston, Oct1976.
• 43: Scott, D. Outline of A Mathematical Theory of Computation. Proc. 4th Annual Princeton Conf. on Information Science & Systems, Princeton, 1970, pp. 169-176.
• 44: Scott, D. and Strachey, C. Toward a Mathematical Semantics for Computer Languages. Proc. of the Symp. on Computers & Automata, Polytech Institute of Brooklyn, New York, 1971, pp. 19-46.
• 45: Scott, D. Data Types as Lattices. SIAM Journal on Computing, 5, 3, September 1976.
• 46: Smullyan, R.M. First-Order Logic. Springer-Verlag, New York, 1968, 158 pp.
• 47: Stenlund, S. Combinators, &lgr;-terms,.and Proof-Theory. D. Reidel, Dordrecht, 1972, 183 pp.
• 48: Trachtenbrot, B.A. O rekursivnoi neotdelimosti, Dokl. Akad. Nauk. SSSR, 88, 1953, pp. 953-956.
• 49: Troelstra, A.S. Metamathematical investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Math, Vol. 344, Verlag, 1973, 485 pp.
• 50: Eric G. Wagner, From algebras to programming languages, Proceedings of the fifth annual ACM symposium on Theory of computing, p.214-223, April 30-May 02, 1973, Austin, Texas, United States [doi>10.1145/800125.804053]
• 51: Mitchell Wand, A new incompleteness result for Hoare's system, Proceedings of the eighth annual ACM symposium on Theory of computing, p.87-91, May 03-05, 1976, Hershey, Pennsylvania, United States [doi>10.1145/800113.803635]
• 52: Wegbreit, B. Constructive Methods in Program Verification to appear IEEE Trans. on software Engineering, 40 pp.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs

Additional Classification:
  F. Theory of Computation
  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, Verification