Constructing Programs Automatically Using Theorem Proving

摘要

The paper describes a method by which programs may be constructed mechanically. The problem of writing a program is transformed into a theorem proving task. The specifications for the program are used to construct a theorem, the theorem is proved, and the program is derived from the proof of the theorem. The specifications for the program are described as a relation between the input and output variables expressed in predicate calculus. Mechanical theorem proving techniques are used to prove the existence of output variables satisfying the specifications. Existence is proven constructively, so that embedded in the proof is a method to compute the desired output values. A program is extracted from the proof. Restrictions to Robinson's resolution principle are proposed so that only constructive proofs are produced. A proof of the soundness of the method is presented. It is also shown that programs for the entire class of recursive functions may be written by automatic program writing. Thus nothing is lost by restricting application of the resolution principle. An implementation of the method which writes LISP programs is described. (Author)