Formalization of Properties of Functional Programs

ABSTRACT

The problems of convergence, correctness, and equivalence of computer programs can be formulated by means of the satisfiability or validity of certain first-order formulas. An algorithm is presented for constructing such formulas for functional programs, i.e. programs defined by LISP-like conditional recursive expressions.

REFERENCES

• 1: CHURCH, A. Introduction to Mathematical Logic, Vol. 1. Princeton U. Press, Princeton, N. J., 1956.
• 2: COOPER, D.C. Program scheme equivalences and second order logic. In Machine Intelligence, Vol. ~, Meltzer, B., and Michie, D. (Eds.), Edinburgh U. Press, Edinburgh, 1969, pp. 3-15.
• 3: FLOYD, R.W. Assigning meaning to programs. In Proc. Symposia in Appl. Math. (1966), Vol. 19 (Schwartz, J. T., Ed.), Amer. Math. Soe., Providence, R. I., 1967, pp. 19-32.
• 4: Zohar Manna, Properties of Programs and the First-Order Predicate Calculus, Journal of the ACM (JACM), v.16 n.2, p.244-255, April 1969 [doi>10.1145/321510.321516]
• 5: --. The correctness of programs. J. Comput. System Sci. 3, 2 (May 1969), 119-127.
• 6: -- AND McCARTHY, J. Properties of programs and partial function logic. In Machine Intelligence, Vol. 5, Michie, D. (Ed.), Edinburgh U. Press, Edinburgh, 1970.
• 7: -- AND PNUELI, A. The validity problem of the 91-function. Memo No. AI-68, Stanford U. Artificial Intelligence Report, Stanford, Calif., Aug. 1968.
• 8: McCARTHY, J. Towards a mathematical science of computation. In Information Processing 1962, Proc. IFIP Congress 62, Popplewell, C. M. (Ed.), North-Holland, Amsterdam, 1963, pp. 21-28.
• 9: --. A basis for a mathematical theory of computation. In Computer Programming and Formal Systems, Braffort, P., and Hirsehberg, D. (Eds.), North-Holland, Amsterdam, 1963, pp. 33-70.
• 10: Elliott Mendelson, Introduction to mathematical logic (3rd ed.), Wadsworth Publ. Co., Belmont, CA, 1987

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

General Terms:
Algorithms, Theory, Verification