基于天使执行的递归函数式程序自自底向上的综合
Bottom-up Synthesis of Recursive Functional Programs using Angelic Execution
摘要：
提出了一种新的自自底向上的【形】的函数递归程序综合方法。虽然自自底向上的【形】的合成技术在某些情况下比自顶向下的方法工作得更好，但没有一种技术可以以纯粹的自自底向上的【形】的方式从逻辑规范合成递归程序。主要的挑战是，有效的自自底向上的【形】方法需要执行正在合成的代码的子表达式，但不可能执行尚未完全构造的程序的递归子表达式。在本文中，我们使用天使语义的概念来解决这一挑战。具体来说，我们的方法找到一个程序，满足规范下天使的语义（我们称之为天使合成），分析其天使执行过程中所作的假设，使用这种分析，以加强规范，并最终重新尝试合成与加强规范。我们提出的天使合成算法是基于版本空间学习，因此有效地处理许多增量合成调用整个算法。我们已经实现了这种方法在一个原型称为突发和评估它的合成问题，从以前的工作。我们的实验表明，突发是能够合成的解决方案，94%的基准在我们的基准套件，优于以前的工作。
英文摘要：
We present a novel bottom-up method for the synthesis of functional recursive programs. While bottom-up synthesis techniques can work better than top-down methods in certain settings, there is no prior technique for synthesizing recursive programs from logical specifications in a purely bottom-up fashion. The main challenge is that effective bottom-up methods need to execute sub-expressions of the code being synthesized, but it is impossible to execute a recursive subexpression of a program that has not been fully constructed yet. In this paper, we address this challenge using the concept of angelic semantics. Specifically, our method finds a program that satisfies the specification under angelic semantics (we refer to this as angelic synthesis), analyzes the assumptions made during its angelic execution, uses this analysis to strengthen the specification, and finally reattempts synthesis with the strengthened specification. Our proposed angelic synthesis algorithm is based on version space learning and therefore deals effectively with many incremental synthesis calls made during the overall algorithm. We have implemented this approach in a prototype called Burst and evaluate it on synthesis problems from prior work. Our experiments show that Burst is able to synthesize a solution to 94% of the benchmarks in our benchmark suite, outperforming prior work.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
