Derived Preconditions and Their Use in Program Synthesis

Loading...
Thumbnail Image
Authors
Smith, Douglas R.
Subjects
theorem proving
deduction
program synthesis
problem reduction
divide and conquer
Advisors
Date of Issue
1982-03
Date
March 1982
Publisher
Monterey, California. Naval Postgraduate School
Language
Abstract
In this paper we pose and begin to explore a deductive problem more general than that of finding a proof that a given goal formula logically follows from a given set of hypotheses. The problem is most simply stated in the propositional calculus: given a goal A and hypothesis H we wish to find a formula P, called a precondition, such that A logically follows from P A H. A precondition pro- vides any additional conditions under which A can be shown to follow from H. A slightly more complex definition of preconditions in a first-order theory is given and used throughout the paper. A formal system based on natural deduction is presented in which preconditions can be derived. A number of examples are then given which show how derived preconditions are used in a program synthesis method we are developing. These uses include theorem proving, formula simplification, simple code generation, the completion of partial specifications for a subalgorithm, and other tasks of a deductive nature.
Type
Technical Report
Description
Series/Report No
Department
Computer Science (CS)
Organization
Naval Postgraduate School
Identifiers
NPS Report Number
NPS52-82-002
Sponsors
Foundation Research Program of the Naval Postgraduate School
Funder
Chief of Naval Research
Format
34 p.
Citation
Distribution Statement
Approved for public release; distribution is unlimited.
Rights
This publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. Copyright protection is not available for this work in the United States.
Collections