Fundamentals of Deductive Program Synthesis

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Aug 01, 1992
Accession Number
ADA461070

Entities

People

  • Richard Waldinger
  • Zohar Manna

Organizations

  • Stanford University

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Artificial Intelligence
  • Computational Science
  • Engineering
  • Information Operations
  • Software Development
  • Specifications
  • Standards
  • Systems Engineering
  • Systems Science

Fields of Study

  • Computer science

Readers

  • Mathematical Modeling and Probability Theory.
  • Systems Analysis and Design