Constructing Induction Rules for Deductive Synthesis Proofs

TLDR

Deductive synthesis promises automated construction of correct programs from specifications, yet synthesizing iterative or recursive programs requires inductive proofs, and existing induction rule techniques are limited to recycling the recursive structure of the specifications. The study aims to develop novel computational techniques that construct induction rules for deductive synthesis proofs, enabling the introduction of novel recursive structures. The authors introduce computational techniques that construct induction rules for deductive synthesis proofs, addressing the limitation that standard methods recycle recursive structures. The combination of rippling and meta‑variables as a least‑commitment device enables novel induction rules.

Abstract

We describe novel computational techniques for constructing induction rules for deductive synthesis proofs. Deductive synthesis holds out the promise of automated construction of correct computer programs from specifications of their desired behaviour. Synthesis of programs with iteration or recursion requires inductive proof, but standard techniques for the construction of appropriate induction rules are restricted to recycling the recursive structure of the specifications. What is needed is induction rule construction techniques that can introduce novel recursive structures. We show that a combination of rippling and the use of meta-variables as a least-commitment device can provide such novelty.