Inductive synthesis theories and algorithms

在“归纳”程序合成领域的研究一直很活跃。归纳方法倾向于通过观察一些预期的输入-输出行为的例子来迭代地计算程序。许多最先进的归纳程序合成技术是基于两个主要组成部分：验证器和合成器。合成器生成候选程序，而验证者（一个人或另一个程序）检查候选程序是否符合高级描述。如果是，则找到正确的程序。否则，验证者向合成器提供一个示例，说明为什么候选程序是不正确的。然后，合成器尝试根据所提供的示例找到另一个程序。这个过程一直持续到找到正确的程序为止。是否达成解决方案是由几个因素决定的，包括高级描述的正确性和提供给合成器的示例的选择。然而，在实践中，高层次的描述往往是片面的，有时是不正确的，从而导致现有的合成算法失败。此外，验证器可以选择的示例集通常是无限的，其元素可能导致合成器搜索效率较低的程序。本论文的总体目标是发展新的归纳综合理论和算法，这些理论和算法(1)解释可能不正确的描述，(2)智能地选择示例，这些示例可以更快地指导合成引擎进行有效的程序。对于前者，重点将放在弱化和强化操作符的设计上，以修复不正确或部分的描述，从而允许生成新的描述(a)在语义上与原始描述相似，并且(b)成功生成正确的程序。对于后者，将定义新的度量标准来度量与合成任务相关的示例的良好性。本论文的研究基础与EPSRC的软件工程研究领域一致。

Research has been active in the area ``inductive" program synthesis. Inductive approaches tend to iteratively compute programs by observing a few examples of expected input-output behaviour. Many state-of-the-art inductive program synthesis techniques are based on two main components: a verifier and a synthesiser. The synthesiser generates a candidate program, whilst a verifier (a human or another program) checks if the candidate meets the high-level description. If so, then a correct program is found. Otherwise, the verifier provides the synthesiser with an example demonstrating why the candidate program is incorrect. The synthesiser then attempts to find an alternative program guided by the example provided. This process continues until a correct program is found. Whether a solution is reached is determined by several factors including the correctness of the high-level description and the choice of examples provided to the synthesiser.However, in practice, high-level descriptions tend to be partial and sometimes incorrect, thus causing existing synthesis algorithms to fail. Furthermore, the set of examples from which a verifier may choose is often infinite, whose elements may lead the synthesiser to search for less efficient programs.The overall aim of this thesis is the development of new inductive synthesis theories and algorithms that (1) account for potentially incorrect descriptions and (2) intelligently select examples that are can direct the synthesis engine to efficient programs more quickly. For the former, the focus will be on the design of weakening and strengthening operators for repairing incorrect or partial descriptions in such a way that allows for new descriptions to be generated that (a) are semantically similar to the original ones, and (b) succeed in yielding a correct program. For the latter, new metrics will be defined to measure the goodness of an example with respect to the synthesis task.The research underlying this thesis is aligned with EPSRC's software engineering research area.