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...

• Type: Conference
• Year: 1999
• Where: KBSE
• Authors: Bernd Fischer 0002, Jon Whittle
• Keywords: Deductive Retrieval, KBSE 1999, Proof Steps, Software Engineering, Synthesis Proof State