The research presented herein proposes a method of program synthesis based on a recursive program schema and performed with an explicit incremental plan as the core of the synthesis. A partial prototype has been built in order to be able to actually perform syntheses according to the method. The presentation of the method is accompanied by examples of performed syntheses.

The program schemata proposed are simple and based directly on the inductive definition of a data structure which is a basis for the program. The replacement rule for instantiating the schemata is also simple. The simple schema and the simple rule should make the method easy to understand.

In situations when program sentences in a program are similar, meaning that there are similarities in their derivations, we would like, if feasible, to avoid constructing all the corresponding derivations. A method to decide when a definition yields analogous sentences and which also produces a substitution defining the analogy is presented. As a result we can replace a derivation by a substitution, making the onus of synthesis easier. The method has been implemented as a part of the system for interactive synthesis support.

The synthesised programs are discussed with three logical concerns in mind as follows: partial correctness, completeness and totality. The synthesised normal programs are always logical consequences of the specification. Whenever the programs and their goals are definite the programs are always partially correct. From a study of the synthesis emerges a sufficient condition for programs that use negation to be partially correct and for definite or normal programs to be complete. Sufficient conditions for the derived relation to be total can be used to show that the program is defined for every element of the recursive set.