Formalization of Properties of Functional Programs
Zohar Manna, Amir Pnueli · Journal of the ACM · 1970
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.