An Improved Program-Synthesizing Algorithm and Its Correctness An improved program-synthesizing algorithm based on the algorithm proposed by Waldinger and Lee in 1969 is given. In the old algorithm, the program-synthesizing problem is translated into a theorem-proving problem, and a program is obtained by analyzing a proof. For the improved algorithm, the analysis is not necessary, and a program is obtained as soon as the proof is completed. This is achieved by using a modified variable tracing mechanism invented by Green in 1969. The correctness of the improved algorithm is also proved; i.e. the program thus obtained always satisfies the specification. CACM April, 1974 Lee, R. C. T. Chang, C. L. Waldinger, R. J. program-synthesizing algorithms, theorem proving, consequence finding, primitive resolutions 3.60 3.64 4.20 4.42 5.21 5.22 5.24 CA740413 JB January 18, 1978 9:32 AM 2657 4 2657 2719 4 2657 2210 5 2657 2657 5 2657 2657 5 2657 2657 5 2657 2719 5 2657 1626 6 2657 210 6 2657 2151 6 2657 2167 6 2657 2210 6 2657 2645 6 2657 2657 6 2657