Fundamentals Of Deductive Program Synthesis
by Waldinger, Richard, Manna, Zohar
Technical Note 503
Institution: AI Center, SRI International
Address: 333 Ravenswood Ave., Menlo Park, CA 94025
Aug 1992.
Note: Published in IEEE Transactions on Software Engineering, v18, n8, August 1992
An informal tutorial is presented for program synthesis, with an emphasis on deductive methods. According to this approach, to construct a program meeting a given specification, we prove the existence of an object meeting the specified conditions. The proof is restricted to be sufficiently constructive, in the sense that, in establishing the existence of the desired output, the proof is forced to indicated a computational method for finding it. That method becomes the basis for a program that can be extracted from the proof. The exposition is based on the deductive-tableau system, a theorem-proving framework particularly suitable for program synthesis. The system includes a nonclausal resolution rule, facilities for reasoning about equality, an a well-founded induction rule.
 Adobe PDF |
 BibTeX |
 EndNote |
| Name | Title | ||
|---|---|---|---|
 |
Waldinger, Richard J | Principal Scientist |  |
