Accession Number:

ADA461070

Title:

Fundamentals of Deductive Program Synthesis

Descriptive Note:

Journal article

Corporate Author:

STANFORD UNIV CA DEPT OF COMPUTER SCIENCE

Personal Author(s):

Report Date:

1992-08-01

Pagination or Media Count:

33.0

Abstract:

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 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 non-causal resolution rule, facilities for reasoning about equality, and a well-founded induction rule.

Subject Categories:

  • Operations Research
  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE