Combining Proof Plans with Partial Order Planning for Imperative Program Synthesis |
| |
Authors: | Andrew Ireland Jamie Stark |
| |
Affiliation: | (1) School of Mathematical & Computer Sciences, Heriot-Watt University, Edinburgh, Scotland, UK |
| |
Abstract: | The structured programming literature provides methods and a wealth of heuristic knowledge for guiding the construction of
provably correct imperative programs. We investigate these methods and heuristics as a basis for mechanizing program synthesis.
Our approach combines proof planning with conventional partial order planning. Proof planning is an automated theorem proving technique which uses high-level proof plans to guide the search for proofs. Proof plans are structured in terms of proof methods, which encapsulate heuristics for guiding proof search. We demonstrate that proof planning provides a local perspective on
the synthesis task. In particular, we show that proof methods can be extended to represent heuristics for guiding program
construction. Partial order planning complements proof planning by providing a global perspective on the synthesis task. This
means that it allows us to reason about the order in which program fragments are composed. Our hybrid approach has been implemented
in a semi-automatic system called Bertha. Bertha supports partial correctness and has been tested on a wide range of non-trivial programming examples. |
| |
Keywords: | proof planning partial order planning deductive synthesis program synthesis |
本文献已被 SpringerLink 等数据库收录! |