
Accession Number : AD0711395
Title : TOWARDS AUTOMATIC PROGRAM SYNTHESIS,
Corporate Author : STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE
Personal Author(s) : Manna,Zohar ; Waldinger,Richard J.
Report Date : JUL 1970
Pagination or Media Count : 56
Abstract : An elementary outline of the theoremproving 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 in efficiency. 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. (Author)
Descriptors : (*COMPUTER PROGRAMMING, *MATHEMATICAL LOGIC), ARTIFICIAL INTELLIGENCE, RECURSIVE FUNCTIONS, ITERATIONS, NUMBERS, THEOREMS
Subject Categories : Theoretical Mathematics
Computer Programming and Software
Distribution Statement : APPROVED FOR PUBLIC RELEASE