Proving Theorems about LISP Functions
Robert S. Boyer, J Strother Moore · Journal of the ACM · 1975
Program verification is the 1den that propertms of programs can be precisely stated and proved in the mathematical sense.In th~s paper, some simple heuristics combimng evaluation and mathematical reduction are described, which the authors have implemented in a program that automatlcally proves a wide varietyof theorems about recursive Lisp functions.The method the program uses to generate induction formulas is described at length The theorems proved by the program include that REVERSE is its own inverse and that a particular SORT program is correct.A list of theorems proved by the program is given KEY WORDS AND PHRASES.