Combining Proof Plans with Partial Order Planning for Imperative Program Synthesis

摘要

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.