Generalized data structure synthesis
Generalized data structure synthesis
复制标题
广义数据结构综合
DOI：
10.1145/3180155.3180211
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Torlak, Emina
中科院分区：
文献类型：
--
作者：
Loncaric, Calvin;Ernst, Michael D.;Torlak, Emina
数据结构综合是根据高级规范生成数据结构实现的任务。该领域的最新工作已显示出节省程序员时间并降低缺陷风险的潜力。现有技术侧重于操作单个集合的子集的数据结构，但现实世界的程序经常跟踪多个相关集合和聚合属性，例如总和、计数、最小值和最大值。本文展示了如何合成跟踪多个相关集合的子集和聚合的数据结构。我们的技术将综合任务分解为查询综合和增量化的交替步骤。查询综合步骤通过利用专门针对数据结构领域的现有枚举综合技术来实现对数据结构状态的纯操作。增量步骤通过将命令性状态修改重新构建为确定要更改的内容的新查询，再加上少量代码来应用更改，从而实现命令式状态修改。与以前的工作相比，这种方法的另一个好处是，合成的数据结构不仅针对规范中的查询进行了优化，而且还针对所需的更新操作进行了优化。我们在四个大型案例研究中评估了我们的方法，证明这些扩展具有广泛的适用性。
Data structure synthesis is the task of generating data structure implementations from high-level specifications. Recent work in this area has shown potential to save programmer time and reduce the risk of defects. Existing techniques focus on data structures for manipulating subsets of a single collection, but real-world programs often track multiple related collections and aggregate properties such as sums, counts, minimums, and maximums.This paper shows how to synthesize data structures that track subsets and aggregations of multiple related collections. Our technique decomposes the synthesis task into alternating steps ofquery synthesisandincrementalization.The query synthesis step implements pure operations over the data structure state by leveraging existing enumerative synthesis techniques, specialized to the data structures domain. The incrementalization step implements imperative state modifications by re-framing them as fresh queries that determine what to change, coupled with a small amount of code to apply the change. As an added benefit of this approach over previous work, the synthesized data structure is optimized for not only the queries in the specification but also the required update operations. We have evaluated our approach in four large case studies, demonstrating that these extensions are broadly applicable.