Provably correct software is one of the key challenges of our software-driven society. Program synthesis -- the task of constructing a program satisfying a given specification -- is one strategy for achieving this. The result of this task is then a program which is correct by design. As in the domain of program verification, handling loops is one of the main ingredients to a successful synthesis procedure. We present an algorithm for synthesizing loops satisfying a given polynomial loop invariant. The class of loops we are considering can be modeled by a system of algebraic recurrence equations with constant coefficients, encoding thus program loops with affine operations among program variables. We turn the task of loop synthesis into a polynomial constraint problem, by precisely characterizing the set of all loops satisfying the given invariant. We prove soundness of our approach, as well as its completeness with respect to an a priori fixed upper bound on the number of program variables. Our work has applications towards synthesizing loops satisfying a given polynomial loop invariant, program verification, as well as generating number sequences from algebraic relations. To understand viability of the methodology and heuristics for synthesizing loops, we implement and evaluate the method using the Absynth tool.
翻译:正确无误的软件是我们软件驱动社会的关键挑战之一。 程序合成 -- -- 构建一个符合特定规格的程序的任务 -- -- 是实现这一目标的一种战略。 任务的结果是一个设计正确的程序。 正如在程序核查领域一样, 处理环是成功合成程序的主要成份之一。 我们展示了一个合成循环的合成算法, 满足给定的多元循环的变异性。 我们考虑的循环类别可以通过一个具有恒定系数的代数复现方程系统进行模拟, 从而将程序循环与程序变量之间的折叠操作进行编码。 我们把环合成的任务转换成一个多重制约问题, 精确地描述满足给定变量的所有环的特性。 我们证明了我们的方法的正确性, 以及它对于程序变量数的先前固定上限的完整性。 我们的工作应用于合成循环系统, 满足给定的多数值循环, 程序核查, 从而在程序变量之间编码程序循环中进行折合操作。 我们把环合成的任务变成一个多数值制约问题, 通过精确地描述满足给定的环形环形的特性, 来评估我们如何运用它的方法, 。