The project deals with program synthesis, the derivation of a program to meet a given specification. While the specification describes the conditions the desired program is to satisfy, the program itself describes a detailed method for meeting those conditions. The benefit of this research is to make the programming process easier and less subject to error. The method is based on a deductive approach, in which the problem of deriving a program is regarded as one of proving a mathematical theorem. The theorem expresses the existence of an object meeting the specified conditions. The proof is restricted to be sufficiently constructive to indicate a method for finding the desired output. That method becomes the basis for a program, which is extracted from the proof. The emphasis of the work has been on automating as much as possible of the program derivation process. In particular, theorem-proving methods particularly well-suited to the program synthesis application have been developed. An experimental interactive program-derivation system is being implemented. Current research topics included developing a more automatic theorem prover, modifying already constructed programs, and controlling the efficiency of derived programs.
