Toward tool support for interactive synthesis
Toward tool support for interactive synthesis
复制标题
为交互式综合提供工具支持
DOI：
10.1145/2814228.2814235
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
D. Culler
中科院分区：
文献类型：
--
作者：
Shaon Barman;Rastislav Bodík;S. Chandra;Emina Torlak;A. Bhattacharya;D. Culler
语法引导综合通过探索大量候选程序来搜索给定规范的实现。草图通过预先定义所需实现的结构来减少这些搜索空间，使综合变得更容易处理。通常，这种结构是通过人类洞察力获得的——本文介绍了一种交互式、工具支持的发现这种结构的方法。关键思想是将规范分解为子计算，以便分解决定草图。我们依赖于一个容易获得的规范，它只不过是一组有限的样本输入输出对或所需程序的执行跟踪。我们引入两个互补分解算子并在案例研究中演示它们。我们发现，我们发现结构的交互式方法将计算机辅助编程的范围扩展到了仅通过综合无法解决的问题。
Syntax-guided synthesis searches for an implementation of a given specification by exploring large spaces of candidate programs. Sketches reduce these search spaces, making synthesis more tractable, by predefining the structure of the desired implementation. Typically, this structure is obtained through human insight---this paper introduces a method for interactive, tool-supported discovery of such structure. The key idea is to decompose the specification into subcomputations such that the decomposition dictates the sketch. We rely on a readily obtainable specification that is nothing more than a finite set of sample input-output pairs or execution traces of the desired program. We introduce two complementary decomposition operators and demonstrate them on case studies. We find that our interactive methodology to discover structure extends the reach of computer-aided programming to problems that cannot be solved with synthesis alone.