来自具有效果库的规范引导的组件化合成
摘要：基于组件的合成旨在利用一组库提供的API构建程序。通常，这些API具有效果，这使得对潜在合成候选的正确性进行推理变得具有挑战性。这是因为由有副作用的库过程对全局状态所做的更改会影响它们如何组合在一起，从而产生一个难以处理的大的搜索空间，可能会困扰典型的枚举合成技术。然而，如果这些效果的性质作为其规范的一部分暴露出来，那么可以使用演绎合成方法来帮助指导组件的搜索。在本文中，我们提出了一种新的规范引导合成程序，它使用Hoare风格的前置条件和后置条件来表达潜在库组件候选的细粒度效果，以驱动双向合成搜索策略。该程序在现有上下文中寻求构建更大项的前向搜索过程和在其他情况下不知道实际目标的后向搜索机制之间交替进行。为了进一步提高效率和可扩展性，我们将一个基于冲突驱动的学习过程集成到合成算法中，该学习过程提供先前遇到的不成功搜索路径的语义表达，并在合成过程中用于修剪可能的候选空间。我们已经在一个名为Cobalt的工具中实现了我们的想法，并在基于OCaml库的有副作用规范上定义的一些具有挑战性的合成问题上展示了其有效性。
作者：Ashish Mishra, Suresh Jagannathan
论文ID：2209.02752
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-09-08