Files in this item



application/pdf9114198.pdf (5MB)Restricted to U of Illinois
(no description provided)PDF


Title:Synthesis of procedural and data abstractions
Author(s):Cheng, Betty Hsiao-Chih
Doctoral Committee Chair(s):Kaplan, Simon M.
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Subject(s):Computer Science
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.
Issue Date:1990
Rights Information:Copyright 1990 Cheng, Betty Hsiao-Chih
Date Available in IDEALS:2011-05-07
Identifier in Online Catalog:AAI9114198
OCLC Identifier:(UMI)AAI9114198

This item appears in the following Collection(s)

Item Statistics