Synthesising recursive functions with side effects

摘要

Automatic Program Synthesis involves the automatic generation of a program (or plan) to achieve a specific goal. This means that smaller pre-defined (or previously synthesised) program segments are combined or modified to achieve the total goal. To guarantee that the required goal is actually achieved, the interactions between these program segments must be identified and considered. This paper shows how the side effects of segments can be derived and constructively used in achieving the required goal, and in guaranteeing the correctness of the resulting program. A program synthesising system PROSYN using these principles will then be described. A trace of a sample program synthesis, which generates a program that solves a general set of linear simultaneous equations, is given in the appendix.