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