The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.08 - August (1992 vol.18)
pp: 674-704
ABSTRACT
<p>An informal tutorial for program synthesis is presented, with an emphasis on deductive methods. According to this approach, to construct a program meeting a given specification, the authors 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 indicate 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, and a well-founded induction rule.</p>
INDEX TERMS
deductive program synthesis; specification; proof; deductive-tableau system; theorem-proving framework; nonclausal resolution rule; reasoning; induction rule; artificial intelligence; formal specification; inference mechanisms; program testing; theorem proving
CITATION
Z. Manna, R. Waldinger, "Fundamentals of Deductive Program Synthesis", IEEE Transactions on Software Engineering, vol.18, no. 8, pp. 674-704, August 1992, doi:10.1109/32.153379
18 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool