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.