Program sketching with live bidirectional evaluation
Program sketching with live bidirectional evaluation
复制标题
通过实时双向评估进行程序草图绘制
DOI：
10.1145/3408991
复制
发表时间：
2020
影响因子：
--
通讯作者：
Chugh, Ravi
中科院分区：
文献类型：
--
作者：
Lubin, Justin;Collins, Nick;Omar, Cyrus;Chugh, Ravi
我们提出了一个系统称为Smyth的程序草图在一个类型化的函数式语言，其中普通断言的具体评价产生的输入输出的例子，然后用来指导搜索完成的漏洞。关键的创新，称为实时双向评估，通过部分评估的草图“向后”传播示例。实时双向评估使Smyth能够（a）合成递归函数而无需跟踪完整的示例集，（B）指定并解决相互依赖的合成目标。消除跟踪完整性的要求解决了一个显着的局限性所面临的先前的合成技术时，部分规格的形式，输入输出examples.To评估我们的技术的实际影响，我们运行了几个实验的基准用来评估神话，一个国家的最先进的基于实例的合成工具。首先，给定专家示例（没有部分实现），我们发现Smyth平均需要Myth所需专家示例数量的66%。其次，我们发现，史密斯是强大的随机生成的例子，合成许多任务与相对较少的随机例子比专家提供的。第三，我们创建了一套小的草图任务，系统地采用简单的草图策略的神话基准，我们发现，用户提供的草图在史密斯往往进一步减少总规范的负担（即部分实现和例子的组合）。最后，我们发现Leon和Synquid，两个最先进的基于逻辑的综合工具，未能完成Smyth成功完成的几项任务。
We present a system called Smyth for program sketching in a typed functional language whereby the concrete evaluation of ordinary assertions gives rise to input-output examples, which are then used to guide the search to complete the holes. The key innovation, called live bidirectional evaluation, propagates examples "backward" through partially evaluated sketches. Live bidirectional evaluation enables Smyth to (a) synthesize recursive functions without trace-complete sets of examples and (b) specify and solve interdependent synthesis goals. Eliminating the trace-completeness requirement resolves a significant limitation faced by prior synthesis techniques when given partial specifications in the form of input-output examples.To assess the practical implications of our techniques, we ran several experiments on benchmarks used to evaluate Myth, a state-of-the-art example-based synthesis tool. First, given expert examples (and no partial implementations), we find that Smyth requires on average 66% of the number of expert examples required by Myth. Second, we find that Smyth is robust to randomly-generated examples, synthesizing many tasks with relatively few more random examples than those provided by an expert. Third, we create a suite of small sketching tasks by systematically employing a simple sketching strategy to the Myth benchmarks; we find that user-provided sketches in Smyth often further reduce the total specification burden (i.e. the combination of partial implementations and examples). Lastly, we find that Leon and Synquid, two state-of-the-art logic-based synthesis tools, fail to complete several tasks on which Smyth succeeds.
登录
查看更多内容
从输入输出示例归纳程序综合
DOI：
--
发表时间：
2016
期刊：
影响因子：
--
作者：
John K. Feser
通讯作者：
John K. Feser
DOI：
10.1007/978-3-540-73589-2_2
发表时间：
2007-07
期刊：
--
影响因子：
--
作者：
Jeremy G. Siek;Walid Taha
通讯作者：
Jeremy G. Siek;Walid Taha
通过类型引导的抽象细化进行程序合成
影响因子：
--
作者：
Guo, Zheng;James, Michael;Justo, David;Zhou, Jiaxiao;Wang, Ziteng;Jhala, Ranjit;Polikarpova, Nadia
通讯作者：
Polikarpova, Nadia
StriSynth：现场编程的综合
DOI：
10.1109/icse.2015.227
发表时间：
2015
期刊：
2015 IEEE/ACM 37th IEEE International Conference on Software Engineering
影响因子：
--
作者：
Sumit Gulwani;M. Mayer;Filip Niksic;R. Piskac
通讯作者：
R. Piskac
逐步打字的细化标准
DOI：
--
发表时间：
2015
期刊：
Summit on Advances in Programming Languages
影响因子：
--
作者：
Jeremy G. Siek;Michael M. Vitousek;M. Cimini;J. Boyland
通讯作者：
J. Boyland