Towards Automatic Imperative Program Synthesis Through Proof Planning

DOI 10.1109/ase.1999.802091 dblp

Abstract

An approach to automatic imperative program synthesis is presented which builds upon Gries' (1981) vision of developing a program and its proof hand in hand. To achieve this vision we rely on the proof planning paradigm, which enables the coupling of both heuristic and deductive components. By formalising structured programming and proof heuristics within the proof planning framework we focus the search for a correct program. Encoding these heuristics within a proof plan and strengthening proof planning, by embedding it within the conventional AI planning paradigm, enables a significant degree of automation.

BibTeX

@inproceedings{Stark-Ireland:ASE99,
  author    = {Jamie Stark and
               Andrew Ireland},
  title     = {Towards Automatic Imperative Program Synthesis Through Proof Planning},
  booktitle = {ASE},
  pages     = {44--51},
  publisher = {{IEEE} Computer Society},
  year      = {1999},
}

Towards Automatic Imperative Program Synthesis Through Proof Planning

Abstract

Related papers