Perfect is the Enemy of Good: Best-Effort Program Synthesis (Artifact)
Perfect is the Enemy of Good: Best-Effort Program Synthesis (Artifact)
复制标题
完美是优秀的敌人：尽力而为的程序综合（神器）
DOI：
10.4230/darts.6.2.16
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
N. Polikarpova
中科院分区：
文献类型：
--
作者：
Hila Peleg;N. Polikarpova
程序综合有望通过从输入输出示例和其他高级规范自动生成代码片段来帮助软件开发人员完成日常任务。传统观点是合成器必须始终准确满足规范。我们推测，这种全有或全无的范例阻碍了采用程序综合作为开发工具：在实践中，用户编写的规范经常包含错误，或者对于综合器来说太难在合理的时间内解决；在这些情况下，用户会得到一个过拟合的结果，或者更常见的是，根本没有结果。在本文中，我们提出了一种新的程序综合范式，我们称之为尽力而为程序综合，其中综合器返回部分有效结果的排序列表，即满足规范某些部分的程序。为了支持这种范例，我们开发了尽力而为枚举，这是一种新的综合算法，它扩展了流行的程序枚举技术，能够以最小的开销累积和返回多个部分有效的结果。我们在名为 Bester 的工具中实现该算法，并根据文献中的 79 个综合基准对其进行评估。与传统观点相反，我们的评估表明，即使规范存在缺陷或太难，Bester 也会返回有用的结果：i）对于规范中存在错误的所有基准，前三个 Bester 结果包含正确的解决方案，ii）对于大多数硬基准测试，前三个结果包含正确解决方案的重要片段。我们还进行了一项探索性用户研究，这证实了我们的直觉，即部分有效的结果是有用的：研究表明程序员使用合成器的输出进行理解，并经常将其合并到他们的解决方案中。
Program synthesis promises to help software developers with everyday tasks by generating code snippets automatically from input-output examples and other high-level specifications. The conventional wisdom is that a synthesizer must always satisfy the specification exactly. We conjecture that this all-or-nothing paradigm stands in the way of adopting program synthesis as a developer tool: in practice, the user-written specification often contains errors or is simply too hard for the synthesizer to solve within a reasonable time; in these cases, the user is left with a single over-fitted result or, more often then not, no result at all. In this paper we propose a new program synthesis paradigm we call best-effort program synthesis , where the synthesizer returns a ranked list of partially-valid results, i.e. programs that satisfy some part of the specification. To support this paradigm, we develop best-effort enumeration , a new synthesis algorithm that extends a popular program enumeration technique with the ability to accumulate and return multiple partially-valid results with minimal overhead. We implement this algorithm in a tool called Bester , and evaluate it on 79 synthesis benchmarks from the literature. Contrary to the conventional wisdom, our evaluation shows that Bester returns useful results even when the specification is flawed or too hard: i ) for all benchmarks with an error in the specification, the top three Bester results contain the correct solution, and ii ) for most hard benchmarks, the top three results contain non-trivial fragments of the correct solution. We also performed an exploratory user study, which confirms our intuition that partially-valid results are useful: the study shows that programmers use the output of the synthesizer for comprehension and often incorporate it into their solutions.
DOI：
--
发表时间：
2017-07
期刊：
ArXiv
影响因子：
--
作者：
Kevin Ellis;Daniel Ritchie;Armando Solar-Lezama;J. Tenenbaum
通讯作者：
Kevin Ellis;Daniel Ritchie;Armando Solar-Lezama;J. Tenenbaum
通过类型引导的抽象细化进行程序合成
影响因子：
--
作者：
Guo, Zheng;James, Michael;Justo, David;Zhou, Jiaxiao;Wang, Ziteng;Jhala, Ranjit;Polikarpova, Nadia
通讯作者：
Polikarpova, Nadia
具有等价约简的程序综合
DOI：
--
发表时间：
2019
期刊：
and Abstract Interpretation
影响因子：
--
作者：
Smith, Calvin;Albarghouthi, Aws
通讯作者：
Albarghouthi, Aws