An Integration of Deductive Retrieval into Deductive Synthesis

10 years 8 months ago
An Integration of Deductive Retrieval into Deductive Synthesis
Deductive retrieval and deductive synthesis are two conceptually closely related software development methods which apply theorem proving techniques to support the construction of correct programs. In this paper, we describe an integration of both methods which combines their complementary benefits and alleviates some of their drawbacks. The core of our integration is an algorithm which automatically extracts queries from the synthesis proof state and submits them to a specialized retrieval system. Retrieved components are then used to close open subgoals in the proof. We use a higher-order framework for synthesis in which higher-order meta-variables are used to represent program fragments still to be synthesized. Hence, the introduction of a new meta-variable is an attempt to synthesize a new fragment and so highlights a possible reuse step. This observation allows us to invoke retrieval only after a substantial change rather than at every proof step and prevents overloading the retr...
Bernd Fischer 0002, Jon Whittle
Added 04 Aug 2010
Updated 04 Aug 2010
Type Conference
Year 1999
Where KBSE
Authors Bernd Fischer 0002, Jon Whittle
Comments (0)