查看文章

Program synthesis is the problem of computing from a specification a program that implements it. New and popular variations on the synthesis problem accept specifications in formats that are easier for the human synthesis user to provide: input–output example pairs, type information, and partial logical specifications. These are all partial specification formats, encoding only a fraction of the expected behavior of the program, leaving many matching programs. This transition into partial specification also changes the mode of work for the user, who now provides additional specifications until they are happy with the synthesis result. Therefore, synthesis becomes an iterative, interactive process. We present a formal model for interactive synthesis, parameterized by an abstract domain of predicates on programs. The abstract domain is used to describe both the iterative refinement of the specifications and reduction of the …