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 95% of the benchmarks in our benchmark suite, outperforming prior work.
翻译:我们提出了一个新的自下而上的方法来综合功能递归程序。 虽然自下而上的合成技术在某些环境中比自上而下的方法可以更好发挥作用, 但在某些环境中, 还没有一种将逻辑规格的循环程序从纯自下而上的方式综合起来的技术。 主要的挑战在于有效的自下而上的方法需要执行正在合成的代码的子表达式, 但是无法执行一个尚未完全构建的程序的循环子表达式。 在本文件中, 我们使用天使语义概念来应对这一挑战。 具体地说, 我们的方法发现一个程序符合天使语义学的规格( 我们称之为天使语义合成), 分析在天使语义执行过程中所作的假设, 使用这种分析来强化该规范, 并最终重新尝试与强化的规范合成。 我们提议的天使合成算法以版本空间学习为基础, 从而有效地处理整个算法中的许多渐进式合成电话。 我们用一个叫作Burst的原型来应对这个方法, 并评估先前工作中的综合问题。 我们的实验显示, Burst 能够将我们的基准化为95 。