Synthesis of procedural and data abstractions

Abstract

Program synthesis is the process of developing a computer program automatically from a specification of its desired behavior. In contrast to software development environments that require the user to write program code, automation shifts the responsibility of the user to the specification phase of program development, potentially increasing productivity by permitting the user to concentrate on high-level design issues. In addition, the program verification process, difficult and time-consuming for existing code, may be performed concurrently with the generation of the code.

This thesis demonstrates, through the construction and the use of the program synthesis system SEED, that it is possible to build an automated program synthesis system that synthesizes complex programs from specifications, verifies their correctness, and stores the results for future use. SEED accepts a formal specification of a problem written in predicate logic and generates annotated program source code satisfying the specification. The rules for choosing which programming language constructs to synthesize are contained in a rule base; background knowledge and domain-specific information are entered into a fact base. During synthesis, SEED uses the fact base to disambiguate rule applications. If no application of rules will yield a satisfactory program, SEED informs the user, who may then modify the specification and restart the synthesis.

In addition to primitive programming language constructs, such as assignment, alternative and iterative statements, SEED is capable of synthesizing recursive and non-recursive procedures and functions, as well as abstract data types. Once SEED has successfully synthesized a procedure, function, or abstract data type, the specification and resultant code are stored in a module library. By storing the results of successful syntheses into a module library, each successful synthesis increases the number of operations available for solving future problems.