Program synthesis is the systematic derivation of a program from a given specification. A deductive approach to program synthesis is presented for the construction of recursive programs.
This paper describes a language for constructing problem-solving programs. The language can manipulate several data structures, including ordered and unordered sets.
This paper develops the following strategy: to achieve two goals simultaneously, develop a plan to achieve one of them and then modify that plan to achieve the second as well.
The deductive approach is a formal program construction method in which the derivation of a program from a given specification is regarded as a theorem-proving task.
Problems in commonsense and robot planning are approached by methods adapted from program synthesis research; planning is regarded as an application of automated deduction.
We describe some of the reasoning and programming capabilities of a projected synthesis system. Special attention is paid to the introduction of conditional tests, loops, and instructions with wide effects in the program being constructed.
Certain similarities between program verification and program synthesis are pointed out. The analogy is illustrated using a "bubble-sort" program. Recent work has shown that automatic deductive methods may be applied to the problems of program verification and program synthesis.
