This item is only available for download by members of the University of Illinois community. Students, faculty, and staff at the U of I may log in with your NetID and password to view the item. If you are trying to access an Illinois-restricted dissertation or thesis, you can request a copy through your library's Inter-Library Loan office or purchase a copy directly from ProQuest.
Permalink
https://hdl.handle.net/2142/22956
Description
Title
Synthesis of procedural and data abstractions
Author(s)
Cheng, Betty Hsiao-Chih
Issue Date
1990
Doctoral Committee Chair(s)
Kaplan, Simon M.
Department of Study
Computer Science
Discipline
Computer Science
Degree Granting Institution
University of Illinois at Urbana-Champaign
Degree Name
Ph.D.
Degree Level
Dissertation
Keyword(s)
Computer Science
Language
eng
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.
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.
