Automatic Synthesis of Recursive Programs: The Proof-Planning Paradigm |
| |
Authors: | Alessandro Armando Alan Smaill Ian Green |
| |
Affiliation: | (1) Dipartimento di Informatica, Sistemistica e Telematica, University of Genova, Via all'Opera Pia 11A, 16145 Genova, Italy;(2) Division of Informatics, University of Edinburgh, 80 South Bridge, Edinburgh, EH1 1HN, Scotland |
| |
Abstract: | We describe a proof method that characterises a family of proofs corresponding to the synthesis of recursive functional programs. This method provides a significant degree of automation in the construction of recursive programs from specifications, together with correctness proofs. This method 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 it with parts of a substantial example—the synthesis of a unification algorithm. |
| |
Keywords: | program synthesis proof-planning middle-out reasoning |
本文献已被 SpringerLink 等数据库收录! |
|