Reverse Sketching

To avoid overwhelming users, many interactive PBE systems only show the highest-ranked programs, even when the system generates tens or hundreds of programs that satisfy the provided examples. Although this approach can significantly reduce the number of candidate programs that a user must consider, it limits their ability to fully understand the solution space and choose the best program for their specific needs. We hypothesize that offering users an overview of the entire space of solutions will help them identify the desired program, even if it is not among the highest ranked ones; identify other, potentially better programs that satisfy the specification; and provide insight into how the synthesizer behaves based on the provided examples, which may help users provide better examples in the future. In this paper, we introduce reverse sketching, a novel algorithm that uses anti-unification to generate a set of sketches, or partially-complete programs with ’holes’, that capture the syntactic structure of multiple programs in the solution space.