Toward Automatic Program Synthesis

An elementary outline of the theorem-proving
approach to automatic program synthesis is given, 
without dwelling on technical details.  The method is
illustrated by the automatic construction of both 
recursive and iterative programs operating on natural
numbers,lists, and trees,  In order to construct 
a program satisfying certain specifications a theorem
induced by those specifications is proved, and 
the desired program is extracted from the proof.  The
same technique is applied to transform recursively 
defined functions into iterative programs, frequently
with a major gain inefficiency.  It is emphasized 
that in order to construct a program with loops or with
recursion, the principle of mathematical induction 
must be applied. The relation between the version of
the induction rule used and the form of the program 
constructed is explored in some detail.

CACM March, 1971

Manna, Z.
Waldinger, R. J.

artificial intelligence, answer extraction, automatic
program synthesis, mathematical induction 
principle, problem solving, theorem proving

3.64 5.23 5.24

CA710302 JB February 3, 1978  4:48 PM

1515	4	2210
2096	4	2210
2127	4	2210
2210	4	2210
1155	5	2210
2210	5	2210
2210	5	2210
2210	5	2210
2657	5	2210
2719	5	2210
1626	6	2210
210	6	2210
2151	6	2210
2167	6	2210
2210	6	2210
2210	6	2210
2645	6	2210
2657	6	2210