Sciweavers

Share
ASE
2006

Combining Proof Plans with Partial Order Planning for Imperative Program Synthesis

11 years 1 months ago
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 im...
Andrew Ireland, Jamie Stark
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2006
Where ASE
Authors Andrew Ireland, Jamie Stark
Comments (0)
books