Programming by predicates: a formal model for interactive synthesis
Programming by predicates: a formal model for interactive synthesis
复制标题
按谓词编程：交互式综合的形式模型
作者：
Hila Peleg;Shachar Itzhaky;Sharon Shoham;Eran Yahav
程序综合是从一个规范计算出实现该规范的程序的问题。综合问题新的流行变体接受对综合用户来说更容易提供的格式的规范：输入 - 输出示例对、类型信息以及部分逻辑规范。这些都是部分规范格式，仅对程序预期行为的一部分进行编码，留下许多匹配的程序。这种向部分规范的转变也改变了用户的工作模式，用户现在要提供额外的规范，直到对综合结果满意为止。因此，综合变成了一个迭代的、交互式的过程。我们提出了一个交互式综合的正式模型，该模型由程序上谓词的一个抽象域参数化。这个抽象域用于描述规范的迭代细化以及候选程序空间的缩减。我们通过表明示例（最常用的规范工具）即使作为完整规范使用时，也是区分程序的一种不充分的工具，从而激发了通过谓词建立一个通用反馈模型的需求。我们使用这个正式模型来描述几个现实世界中的综合器的行为。此外，我们提出了综合会话终止的两个条件，一个仅取决于可用的部分规范的属性，另一个还取决于用户的行为。最后，我们展示了用户意图可实现性的条件，并展示了当一个会话显然要失败时回溯的局限性。
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 candidate program space. We motivate the need for a general feedback model via predicates by showing that examples, the most frequent specification tool, are an insufficient tool to differentiate between programs, even when used as a full specification. We use the formal model to describe the behavior of several real-world synthesizers. Additionally, we present two conditions for termination of a synthesis session, one hinging only on the properties of the available partial specifications, and the other also on the behavior of the user. Finally, we show conditions for realizability of the user’s intent, and show the limitations of backtracking when it is apparent a session will fail.