Automatic Synthesis of Recursive Programs: The Proof-Planning Paradigm

Alessandro Armando, Alan Smaill, Ian Green

DOI 10.1109/ase.1997.632818 dblp

Abstract

We describe a proof plan that characterises a family of proofs corresponding to the synthesis of recursive functional programs. This plan provides a significant degree of automation in the construction of recursive programs from specifications, together with correctness proofs. This plan makes use of meta-variables to allow successive refinement of the identity of unknowns, and so allows the program and the proof to be developed hand in hand. We illustrate the plan with parts of a substantial example-the synthesis of a unification algorithm.

BibTeX

@inproceedings{Armando-al:ASE97,
  author    = {Alessandro Armando and
               Alan Smaill and
               Ian Green},
  title     = {Automatic Synthesis of Recursive Programs: The {Proof-Planning} Paradigm},
  booktitle = {ASE},
  pages     = {2--9},
  publisher = {{IEEE} Computer Society},
  year      = {1997},
}

Automatic Synthesis of Recursive Programs: The Proof-Planning Paradigm

Abstract

Related papers