Inductive Synthesis of Equational Programs

An equational approach to the synthesis of functional and logic programs is taken. Typically, a target program contains equations that are only true in the standard model of the given domain rules. To synthesize such programs, induction is necessary. We propose heuristics for generalizing from a sequence of deductive consequences. These are combined with rewrite-based methods of inductive proof to derive provably correct programs. Introduction Various approaches to the automated synthesis of computer programs have been taken; see [Barr and Feigenbaum, 1981--1982, Chap. X]. In particular, deductive methods have been used to derive executable programs from formal specifications; early examples of such an approach include [Burstall and Darlington, 1977; Manna and Waldinger, 1979]. Inductive, examplebased methods have also been applied to this task; a survey of this approach is [Smith, 1980]; more recent work includes [Shapiro, 1983]. In this paper, we employ both deductive and inductive ..