RbSyn: type- and effect-guided program synthesis
RbSyn: type- and effect-guided program synthesis
复制标题
RbSyn：类型和效果引导的程序合成
DOI：
10.1145/3453483.3454048
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Van Horn, David
中科院分区：
文献类型：
--
作者：
Guria, Sankha Narayan;Foster, Jeffrey S.;Van Horn, David
近年来，研究人员探索了基于组件的合成，其目标是通过组合对现有API的调用来自动构建可运行的程序。然而，先前的工作没有考虑具有副作用的方法的有效合成，例如更新数据库的网络应用方法。在本文中，我们介绍了一个新的类型和效果制导的Ruby合成工具RbSyn。RbSyn合成目标被指定为目标方法的类型以及它必须通过的一系列测试用例。RbSyn的工作方式是递归生成类型良好的候选方法体，其写入效果与测试用例断言的读取效果相匹配。在找到一组分别满足每个测试的候选代码后，RbSyn将合成一个解决方案，该解决方案将分支以在适当的条件下执行正确的候选代码。我们在一个核心的、面向对象的语言RubySynn上形式化了RbSyn，并描述了该模型的关键思想在我们的λ实现中是如何放大的。我们对RbSyn进行了19项基准测试，其中12项来自流行的开源Ruby应用程序。我们发现，RbSyn为所有基准综合了正确的解决方案，15个基准综合在9秒内，而最慢的基准需要83秒。使用观察到的阅读来指导合成是有效的：在12个应用程序基准中，仅使用类型指导就有10个超时。我们还发现，使用不太精确的效果注释会导致较差的合成性能。总而言之，我们认为类型和效果指导的合成是从测试用例中合成有效方法的重要一步。
In recent years, researchers have explored component-based synthesis, which aims to automatically construct programs that operate by composing calls to existing APIs. However, prior work has not considered efficient synthesis of methods with side effects, e.g., web app methods that update a database. In this paper, we introduce RbSyn, a novel type- and effect-guided synthesis tool for Ruby. An RbSyn synthesis goal is specified as the type for the target method and a series of test cases it must pass. RbSyn works by recursively generating well-typed candidate method bodies whose write effects match the read effects of the test case assertions. After finding a set of candidates that separately satisfy each test, RbSyn synthesizes a solution that branches to execute the correct candidate code under the appropriate conditions. We formalize RbSyn on a core, object-oriented language λsynand describe how the key ideas of the model are scaled-up in our implementation for Ruby. We evaluated RbSyn on 19 benchmarks, 12 of which come from popular, open-source Ruby apps. We found that RbSyn synthesizes correct solutions for all benchmarks, with 15 benchmarks synthesizing in under 9 seconds, while the slowest benchmark takes 83 seconds. Using observed reads to guide synthesize is effective: using type-guidance alone times out on 10 of 12 app benchmarks. We also found that using less precise effect annotations leads to worse synthesis performance. In summary, we believe type- and effect-guided synthesis is an important step forward in synthesis of effectful methods from test cases.
登录
查看更多内容
动态语言的即时静态类型检查
DOI：
10.1145/2908080.2908127
发表时间：
2016
期刊：
Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation
影响因子：
--
作者：
Brianna M. Ren;J. Foster
通讯作者：
J. Foster
影响因子：
--
作者：
Yu Feng;R. Martins;O. Bastani;Işıl Dillig
通讯作者：
Yu Feng;R. Martins;O. Bastani;Işıl Dillig
效果作为功能：效果处理程序和轻量级效果多态性
影响因子：
--
作者：
J. Brachthäuser;Philipp Schuster;K. Ostermann
通讯作者：
K. Ostermann
论程序规范中的框架问题
DOI：
--
发表时间：
1995
期刊：
IEEE Trans. Software Eng.
影响因子：
--
作者：
Alexander Borgida;J. Mylopoulos;R. Reiter
通讯作者：
R. Reiter
Ruby on Rails 数据模型的有限验证
DOI：
10.1145/2001420.2001429
发表时间：
2011
期刊：
Proceedings of the 2015 International Symposium on Software Testing and Analysis
影响因子：
--
作者：
J. Nijjar;T. Bultan
通讯作者：
T. Bultan