David Cristina, Kroening Daniel
Department of Computer Science, University of Oxford, Oxford, UK.
Department of Computer Science, University of Oxford, Oxford, UK
Philos Trans A Math Phys Eng Sci. 2017 Oct 13;375(2104). doi: 10.1098/rsta.2015.0403.
Program synthesis is the mechanized construction of software, dubbed 'self-writing code'. Synthesis tools relieve the programmer from thinking about how the problem is to be solved; instead, the programmer only provides a description of what is to be achieved. Given a specification of what the program should do, the synthesizer generates an implementation that provably satisfies this specification. From a logical point of view, a program synthesizer is a solver for second-order existential logic. Owing to the expressiveness of second-order logic, program synthesis has an extremely broad range of applications. We survey some of these applications as well as recent trends in the algorithms that solve the program synthesis problem. In particular, we focus on an approach that has raised the profile of program synthesis and ushered in a generation of new synthesis tools, namely counter-example-guided inductive synthesis (CEGIS). We provide a description of the CEGIS architecture, followed by recent algorithmic improvements. We conjecture that the capacity of program synthesis engines will see further step change, in a manner that is transparent to the applications, which will open up an even broader range of use-cases.This article is part of the themed issue 'Verified trustworthy software systems'.
程序合成是软件的机械化构建，即所谓的“自编写代码”。合成工具使程序员无需思考如何解决问题；相反，程序员只需提供对要实现目标的描述。给定程序应执行的规范，合成器会生成一个可证明满足该规范的实现。从逻辑角度来看，程序合成器是二阶存在逻辑的求解器。由于二阶逻辑的表达能力，程序合成具有极其广泛的应用范围。我们将概述其中一些应用以及解决程序合成问题的算法的最新趋势。特别是，我们将重点关注一种提升了程序合成知名度并催生了新一代合成工具的方法，即反例引导的归纳合成（CEGIS）。我们将描述CEGIS架构，随后介绍最近的算法改进。我们推测，程序合成引擎的能力将进一步实现跨越式发展，且这种发展对应用来说是透明的，这将开辟更广泛的用例范围。本文是主题为“经过验证的可信软件系统”的特刊的一部分。
