A Study in Automatic Programming

摘要

A description of methods and an implementation of a system for automalic generation of programs is given. The problems of writing programs for numerical computation, symbol manipulation, robot control and everyday planning have been studied and some programs generated. A particular formalism, i.e. a FRAME, has been developed to define the programming environment and permit the statement of a problem. A frame, F _ is formulated within the Logic of Prot_rams [Hoare 1969, Hoare and Wirth 1972] and includes primitive functions and procedures, axioms, definitions and rules of program composition. Given a frame, F, a problem for program constuction may be stated as a pair <],G>, where] is an input assertion and G is an output assertion. The program generation task is to construct a program A such that I{A}r, where I ': _ G. This process may be viewed as a search in the Logic of Programs for a proof that the generated program satisfies the given input-output assertions. Correctness of programs generated using the formal algorithm is discussed. A frame is translated into a backtrack problem solver augmented by special search procedures. The system is interactive, responds to simple advice and allows incremental and structured program development. The output or solution program is a subset of ALGOL containing procedure calls, assignments, while loops and conditional statements. This research was largely done at Stanford University as the author's Ph.D.Thesis.