规范引导的基于可靠库的综合
Specification-Guided Component-Based Synthesis from Effectful Libraries
摘要：
基于编译器的合成寻求使用一组库提供的API来构建程序。通常，这些API具有影响，这使得推理潜在合成候选者的正确性具有挑战性。这是因为由有效的库过程对全局状态所做的更改会影响它们如何组合在一起，从而产生难以处理的大搜索空间，这会混淆典型的枚举合成技术。然而，如果这些效应的性质作为其规格的一部分被暴露，则可以使用演绎综合方法来帮助指导对组件的搜索。在本文中，我们提出了一个新的规范指导的综合过程，使用霍尔风格的前，后条件来表达潜在的库组件候选人的细粒度的影响，以驱动一个双向的综合搜索策略。该过程在前向搜索过程与后向搜索机制之间交替，前向搜索过程寻求在给定现有上下文的情况下构建更大的术语，但是前向搜索过程不知道实际目标，后向搜索机制寻求与期望目标一致的术语，但是后向搜索机制不知道这些术语必须从其合成的上下文。为了进一步提高效率和可扩展性，我们将冲突驱动的学习过程集成到合成算法中，该合成算法提供了先前遇到的不成功的搜索路径的语义表征，用于修剪可能的候选人的空间，作为合成的进行。我们已经实现了我们的想法，在一个名为Cobalt的工具，并证明了它的有效性上的一些具有挑战性的合成问题，定义在OCaml库配备有效的规范。
英文摘要：
Component-based synthesis seeks to build programs using the APIs provided by a set of libraries. Oftentimes, these APIs have effects, which make it challenging to reason about the correctness of potential synthesis candidates. This is because changes to global state made by effectful library procedures affect how they may be composed together, yielding an intractably large search space that can confound typical enumerative synthesis techniques. If the nature of these effects are exposed as part of their specification, however, deductive synthesis approaches can be used to help guide the search for components. In this paper, we present a new specification-guided synthesis procedure that uses Hoare-style pre- and post-conditions to express fine-grained effects of potential library component candidates to drive a bi-directional synthesis search strategy. The procedure alternates between a forward search process that seeks to build larger terms given an existing context but which is otherwise unaware of the actual goal, alongside a backward search mechanism that seeks terms consistent with the desired goal but which is otherwise unaware of the context from which these terms must be synthesized. To further improve efficiency and scalability, we integrate a conflict-driven learning procedure into the synthesis algorithm that provides a semantic characterization of previously encountered unsuccessful search paths that is used to prune the space of possible candidates as synthesis proceeds. We have implemented our ideas in a tool called Cobalt and demonstrate its effectiveness on a number of challenging synthesis problems defined over OCaml libraries equipped with effectful specifications.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
