The programming by example approach of [1]} learns programs from
input-output examples and relies on lightweight interaction to refine the
specification of programs to be specified. The approach has further been
extended in [2]} with machine learning, allowing to learn
programs from just one (or even none) input-output example by using a simple
supervised learning setup. Program synthesis from input-output examples is shown
to be successful for recursive programs [3]}, yet synthesizing
loops and handling non-linear arithmetic is not yet supported by this
line of research.
Our work does not learn programs from
observed input-output examples, but uses loop invariants to fully characterize
the intended behavior of the program to be synthesized. We precisely
characterize the solution space of loops to be synthesized by a system of
algebraic recurrences, without using statistical models supporting
machine learning. Thanks to its precision, our method is however computationally
more expensive and does not yet scale to large programs/data sets.
