MPI-INF Logo
MPI-INF/SWS Research Reports 1991-2017

2. Number - only D2

MPI-I-93-231

A framework for program development based on schematic proof

Basin, David A. and Bundy, Alan and Kraan, Ina and Matthews, Seán

August 1993, 12 pages.

.
Status: available - back from printing

Often, calculi for manipulating and reasoning about programs can be recast as calculi for synthesizing programs. The difference involves often only a slight shift of perspective: admitting metavariables into proofs. We propose that such calculi should be implemented in logical frameworks that support this kind of proof construction and that such an implementation can unify program verification and synthesis. Our proposal is illustrated with a worked example developed in Paulson's Isabelle system. We also give examples of existent calculi that are closely related to the methodology we are proposing and others that can be profitably recast using our approach.
Categories / Keywords:
program synthesis, program verification, program transformation, logical frameworks, deductive synthesis, higher-order unification

URL to this document: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1993-231

Hide details for BibTeXBibTeX
@TECHREPORT{BasinBundyKraanMatthews93,
  AUTHOR = {Basin, David A. and Bundy, Alan and Kraan, Ina and Matthews, Se{\'a}n},
  TITLE = {A framework for program development based on schematic proof},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-93-231},
  MONTH = {August},
  YEAR = {1993},
  ISSN = {0946-011X},
}