The automatic synthesis of recursive programs

We describe a deductive technique for the automatic construction of recursive programs to meet given input-output specifications. These specifications express what conditions the output of the desi...