Derived Preconditions and Their Use in Program Synthesis
Smith, Douglas R.
MetadataShow full item record
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.
RightsThis 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.
NPS Report NumberNPS52-82-002
Showing items related by title, author, creator and subject.
Davis, Rachel N. (Monterey, California: Naval Postgraduate School, 2014-03);The economic factors in the Arab'Israeli Conflict are often overshadowed by its more powerful political features, but economics plays a significant, if not equal, role in the conflict's protracted nature. Like politics, ...
A calorimetric study of the microstructures of a thermomechanically processed Al-10.0% Mg-0.1% Zr alloy. Andrews, James N. Jr. (1986-09);DifTerential scanning calorimetry (DSC) was used to investigate microstructure evolution in a high-magnesium aluminum-magnesium alloy, Al-10.0% Mg-0.1% Zr, which had been thermomechanically processed. The two variations ...
Henley, Curtis D.; Hunt, Shaun C.; Phillips, Darius A. (Monterey California. Naval Postgraduate School, 2007-12);The objective of this Joint Applied Project was to analyze the feasibility for production of renewable energy on DoD installations and focus on renewable energy initiatives undertaken at Nellis AFB, NV. This project ...