Invariants are key to formal loop verification as they capture loop properties that are valid before and after each loop iteration. Yet, generating invariants is a notorious task already for syntactically restricted classes of loops. Rather than generating invariants for given loops, in this paper we synthesise loops that exhibit a predefined behaviour given by an invariant. From the perspective of formal loop verification, the synthesised loops are thus correct by design and no longer need to be verified. To overcome the hardness of reasoning with arbitrarily strong invariants, in this paper we construct simple (non-nested) while loops with linear updates that exhibit polynomial equality invariants. Rather than solving arbitrary polynomial equations, we consider loop properties defined by a single quadratic invariant in any number of variables. We present a procedure that, given a quadratic equation, decides whether a loop with affine updates satisfying this equation exists. Furthermore, if the answer is positive, the procedure synthesises a loop and ensures its variables achieve infinitely many different values.

翻译：不变式是形式化循环验证的关键，它们捕获了循环在每次迭代前后均保持不变的属性。然而，即使对于句法受限的循环类别，生成不变式也是一项具有挑战性的任务。本文并非为给定循环生成不变式，而是综合出具有由不变式定义的预定行为的循环。从形式化循环验证的角度看，此类综合所得的循环在设计上即是正确的，无需再进行验证。为了克服使用任意强不变式进行推理的困难性，本文构造了具有线性更新的简单（非嵌套）while循环，这些循环具有多项式等式不变式。我们并非求解任意多项式方程，而是考虑由单一二次不变式定义的循环属性（变量数目任意）。我们提出了一种过程：给定一个二次方程，该过程能够判定是否存在满足该方程的具有仿射更新的循环。此外，若答案为是，该过程将综合出一个循环，并确保其变量能够取得无限多个不同的值。