A Dynamic Approach to Characterizing Termination of General Logic Programs
本文给出了一般逻辑程序终止性的一个新的刻画。大多数现有的终止分析方法依赖于关于逻辑程序的源代码的结构的一些静态信息，诸如模式/类型、范数/级别映射、模型/参数间关系等。我们提出了一个动态的方法，它采用了一些关键的动态功能的无限（广义）SLDNF衍生，如重复选定的子目标和递归增加长期的大小。我们还介绍了一种新的制定SLDNF树，称为广义SLDNF树。广义SLDNF-树以与Prolog相同的方式处理负子目标，并且存在于任何一般逻辑程序中。
2002-04-12 cs.LO cs.PL
Verifying Termination and Error-Freedom of Logic Programs with block Declarations
我们提出了延迟声明的逻辑程序的验证方法。验证的性质是终止和自由的错误有关的内置。关于终止，我们提出了两种方法。第一种方法试图消除众所周知的推测性输出绑定问题。第二种方法是基于识别的谓词，使用这个谓词的原子的文本位置是无关的终止。这项工作有三个特点：它允许在几种模式下使用谓词;它表明块声明，这是一个非常简单的延迟结构，足以确保所需的属性;它考虑到选择规则，假设它是在大多数Prolog实现。这些方法可用于验证现有程序和帮助编写新程序。
2000-06-23 cs.LO cs.PL
Semantics and Termination of Simply-Moded Logic Programs with Dynamic Scheduling
在逻辑编程中，动态调度是指在运行时确定每个解析（计算）步骤中原子的选择的情况，而不是像Prolog中从左到右的选择规则。这在例如并行编程中具有应用。在现有的语言中，以延迟声明的形式提供了一种控制动态调度的机制。在抽象技术细节的同时，引入了消耗输入的推导来描述动态调度。在本文中，我们首先正式延迟声明和输入消费派生之间的关系，在许多情况下，一对一的对应关系。然后，我们定义了一个模型理论的语义输入消费派生的简单模式的程序。最后，对于这类程序，我们提供了一个终止的充分必要条件。
2001-01-23 cs.LO cs.PL
A Calculus for Modular Loop Acceleration and Non-Termination Proofs
循环加速可以用来证明程序的安全性、可达性、运行时界限和（非）终止性。为此，已经提出了各种加速技术。然而，到目前为止，所有这些都是单一的，即，不能使用几种不同加速技术的组合来加速单个循环。相比之下，我们提出了一个演算，允许以模块化的方式结合加速技术，我们展示了如何将许多现有的加速技术集成到我们的演算。此外，我们提出了两种新的加速技术，可以无缝地纳入我们的微积分。其中一些加速技术仅适用于非终止循环。因此，将它们与我们的新演算相结合，产生了一种新的模块化方法来证明非终止性。实证评估表明，我们的方法的适用性，无论是循环加速和证明不终止。
2022-06-08 cs.LO cs.PL
Inference of termination conditions for numerical loops
本文提出了一种新的分析逻辑程序中数值计算终止性的方法。传统的方法由于整数的非良基性而无法对其进行分析。我们提出了一种技术，可以克服这些困难。我们的方法是基于转换程序的方式，允许集成和扩展技术最初开发的数值计算分析的框架中的查询映射对与知名的框架的可接受性。这样的整合不仅有助于理解终止行为的数值计算，但也允许自动执行正确的分析，这样的计算，从而扩展以前的工作基于约束的方法终止。在本文的最后一节中，我们讨论了可能的扩展技术，包括将一般的长期订单。
2001-06-26 cs.LO cs.PL
Memoisation: Purely, Left-recursively, and with (Continuation Passing) Style
UCL（伦敦大学学院）；Jukedeck Ltd.（Jukedeck有限公司）
Memoisation或制表是一种众所周知的技术，可以大大提高某些递归计算的性能。Prolog语言中的表分解可以将所谓的左递归谓词从非终止计算转化为有限的、行为良好的谓词。在函数式编程文献中，memoisation通常是以不处理左递归的方式实现的，需要补充机制来防止非终止性。一个值得注意的例外是Johnson（1995）在Scheme中的连续传递方法。然而，这依赖于备忘录表数据结构的变化和以显式连续传递风格的编码。我们展示了如何约翰逊的方法可以实现纯功能的现代，强类型的函数语言（OCaml），通过一个一元接口，隐藏的实现细节，但提供了一种方法来返回一个紧凑的表示的备忘录表在计算结束。
2017-07-15 cs.CL cs.LO cs.PL
While Loops in Coq
本文提出在 Coq 浅层嵌入的命令式语言中引入 while 循环的方法，通过一种可定义可能不终止递归函数的通用技术解决 Coq 对终止证明的要求，并以链表程序验证其有效性。
2023-09-25 cs.LO cs.PL
Termination Analysis of General Logic Programs for Moded Queries: A Dynamic Approach
逻辑程序的终止问题可以用静态或动态的方法来解决。静态方法在编译时执行终止分析，而动态方法通过应用循环检查技术来表征和测试逻辑程序的终止。在本文中，我们提出了一种新的动态方法，终止分析一般逻辑程序与模态查询。我们解决了几个有趣的问题，包括如何制定一个SLDNF派生的moded查询，如何表征一个无限的SLDNF派生的moded查询，以及如何应用循环检查机制，以削减无限的SLDNF派生的终止分析的目的。所提出的方法非常强大和有用。它可以用来（1）测试一个逻辑程序是否终止于一个给定的具体或模态查询，（2）测试一个逻辑程序是否终止于所有的具体或模态查询，以及（3）找到所有（最一般的）最有可能终止（或非终止）的具体/模态查询。
2005-12-14 cs.LO cs.PL
Characterization of Termination for Linear Loop Programs
给出了线性齐次规划终止的充分必要条件。我们还开发了一个完整的方法来检查这类程序的终止性。我们的完整表征终止这样的程序是基于线性代数方法。我们减少了验证的终止问题，以检查一个确定的向量空间和一定的向量，都涉及到程序中的循环的正交性。此外，我们提供的理论结果和象征性的计算方法，保证的合理性，完整性和数值稳定性的方法。最后，我们表明，它是足够的解释变量值在一个特定的可数数域，甚至在其环的整数，当一个人想要检查终止的实数。
2014-09-10 cs.PL
Ghost Signals: Verifying Termination of Busy-Waiting (Extended Version)
多处理器机器的程序通常执行忙等待同步。我们提出了第一个分离逻辑模块化验证终止的公平调度下，这样的程序。我们的逻辑要求证明作者将虚信号与每个忙等待循环相关联，并允许这样的循环在其相应的信号$s$未设置时停止。证明作者还必须对信号定义有根据的顺序，并证明如果循环线程持有设置信号$s^\prime$的义务，则$s^\prime$的顺序高于$s$。通过使用传统的共享状态不变量将重影信号的状态与数据结构的状态相关联，可以验证在任意数据结构上忙等待任意条件的程序。
2021-05-18 cs.LO cs.PL
Almost-Sure Termination by Guarded Refinement
本文提出Caliper，一种基于受保护递归和概率耦合的高阶分离逻辑，通过证明程序与简单模型间的精化来建立概率程序的几乎必然终止，并在Coq中验证多个示例。
2024-11-11 cs.LO cs.PL
Reflections on Termination of Linear Loops
本文展示了如何线性动力系统的技术可以用来推理一般循环的行为。我们提出了两个主要结果。首先，我们证明了每一个可以表示为线性整数运算中的转换公式的循环都有一个最佳模型作为确定性仿射转换系统。其次，我们证明了，对于任何线性动力系统$f$与整数特征值和任何整数算术公式$G$，有一个线性整数算术公式，恰好为$G$的状态，其中$f$最终不变。结合这两个，我们开发了一个单调的条件终止分析一般循环。
2021-05-28 cs.PL
Non-Termination Inference of Logic Programs
本文提出了一种逻辑程序非终止推理的静态分析技术。我们的框架依赖于包容测试的扩展，其中一些特定的参数位置可以被实例化，而另一些则被泛化。我们给出的语法标准，静态地确定这样的参数位置从一个程序的文本。原子左循环查询从感兴趣的程序的二进制展开的选定子集自底向上生成。我们提出了一套正确的算法自动化的方法。然后，非终止推理是定制的，试图证明左终止条件计算的终止推理工具的最优性。实验评估报告。当终止性和非终止性分析为逻辑过程产生互补的结果时，则相对于最左边的选择规则和用于描述原子查询集的语言，每个分析都是最优的，并且它们一起引起逻辑过程的操作行为的表征。
2004-06-22 cs.LO cs.PL
Modular Verification for Almost-Sure Termination of Probabilistic Programs
在这项工作中，我们考虑几乎肯定终止问题的概率程序，询问是否一个给定的概率程序终止概率为1。可伸缩的程序分析方法通常依赖于模块化作为其理论基础。在非概率程序中，Floyd-霍尔逻辑的经典变式规则（V-规则）为模块化分析提供了基础。将该规则扩展到概率程序的几乎确定终止是相当棘手的，并且在[Fioriti and Hermanns 2015]中提出了一个概率变体。虽然所提出的概率变量谨慎地解决了可积性的关键问题，我们表明，所提出的模块化规则仍然是不健全的几乎肯定终止的概率程序。除了建立以前的规则的不健全，我们的贡献如下：首先，我们提出了一个健全的模块规则几乎确定终止的概率程序。我们的方法是基于一个新的概念下降上鞅。其次，对于算法方法，我们考虑下降上鞅是线性的，并表明它们可以在多项式时间合成。最后，我们提出了各种基准测试和几个自然的例子，模拟各种类型的嵌套而循环的概率程序的实验结果，并证明我们的方法是能够有效地证明其几乎肯定的终止属性。
2019-08-12 cs.LO cs.PL
SLT-Resolution for the Well-Founded Semantics
全局SLS-归结和SLG-归结是自顶向下评价一般逻辑程序良基语义的两种典型机制。全局SLS解析对于查询评估是线性的，但是遭受无限循环和冗余计算。相比之下，SLG-归结通过制表来解决无限循环和冗余计算，但它不是线性的。非线性方法的主要缺点是，它不能使用简单，有效的基于堆栈的内存结构来实现，也不能很容易地扩展到处理一些严格的顺序运算符，如Prolog中的cuts。在本文中，我们提出了一个线性制表方法，称为SLT-分辨率，自顶向下的评价良好的基础语义。SLT-分辨率是SLDNF-分辨率与制表的实质性扩展。它的主要特点包括：（1）在保持线性的同时，解决了无限循环和冗余计算问题。(2)它是终止的，声音和完整的w.r.t.有界项大小属性与非挣扎查询的程序的良基语义。它的时间复杂度与无函数逻辑程序的SLG-归结和多项式相当。(3)由于它的线性查询评估，SLT-分辨率的桥梁之间的差距，良好的基础语义和标准的Prolog实现技术。它可以通过扩展到任何现有的Prolog抽象机器（如WAM或ATOAM）来实现。
2001-03-02 cs.AI cs.PL
The Automatic Synthesis of Linear Ranking Functions: The Complete Unabridged Version
证明通用顺序计算机程序终止的经典技术涉及程序的每个循环的排序函数的合成。线性排名函数特别有趣，因为许多终止循环都允许线性排名函数，并且存在自动合成线性排名函数的算法。本文提出了两种这样的算法：一种基于Sohn和Van Gelder 1991年的工作;另一种是Podelski和Rybalchenko于2004年提出的。值得注意的是，虽然这两种算法将在完全相同的条件下合成一个线性排序函数，但前者大多是未知的终止分析社区，其普遍适用性在本文之前从未提出过。在本文中，我们彻底证明这两种算法，我们证明了他们的正确性，我们比较他们的最坏情况下的复杂性和实验评估其效率，我们提出了一个开源的实现，他们将很容易包括终止分析功能的自动程序验证。
2012-04-01 cs.LO cs.PL
The Probabilistic Termination Tool Amber
我们描述了琥珀工具证明和反驳终止一类概率的同时，程序与多项式算术，在一个完全自动化的方式。Amber将鞅理论与渐近边界函数的性质相结合，并实现了现有概率终止证明规则的放松版本，以证明/反驳概率循环的（正）几乎必然终止。Amber支持由符号常量参数化的程序，并从常见的概率分布中绘制。我们的实验比较给出了Amber优于现有最先进工具的实际证据。
2021-07-27 cs.PL
The nature of loops in programming
本文提出用 Noetherian 关系的极限统一定义循环，证明时只需识别该关系即可同时保证部分正确性与终止性，无需分别构造不变量和变体。
2025-04-10 cs.PL cs.SE
A Calculus for Modular Loop Acceleration
循环加速可以用来证明安全性、可达性、运行时界限和对整数进行操作的程序的（非）终止性。为此，已经提出了各种加速技术。然而，它们都是整体的：要么成功地加速循环，要么完全失败。相比之下，我们提出了一个演算，允许以模块化的方式结合加速技术，我们展示了如何将许多现有的加速技术集成到我们的演算。此外，我们提出了两种新的加速技术，可以无缝地纳入我们的微积分。实证评估表明，我们的方法的适用性。
2020-02-20 cs.LO cs.PL
Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time
程序敏感性（也称为Lipschitz连续性）的概念规定程序输入的变化会导致程序输出成比例的变化。对于概率程序，这个概念自然地扩展到期望灵敏度。以前的方法开发了一个关系程序逻辑框架，用于证明概率while循环的预期灵敏度，其中迭代次数是固定的和有界的。在这项工作中，我们考虑概率while循环的迭代次数不是固定的，而是随机的，并取决于初始输入值。我们提出了一个合理的方法来证明预期的敏感性，这样的程序。我们的声音方法是基于鞅的，可以通过现有的鞅合成算法自动化。此外，我们的方法是组合的，而循环的顺序组成下一个温和的侧条件。我们证明了我们的方法的有效性，从赌徒的破产，随机混合动力系统和随机梯度下降几个经典的例子。我们还提出了实验结果表明，我们的自动化方法可以处理各种概率的程序在文献中。
2019-10-28 cs.PL
Eventual Linear Ranking Functions
程序终止性是程序分析中的一个研究热点。在过去的几年里，已经见证了用于程序设计语言（如C和Java）的终止分析器的发展，其具有显著的精度和性能。这些系统在很大程度上是基于来自声明式约束编程领域的技术和工具。在本文中，我们首先回顾了一个算法的基础上法卡斯引理发现线性排名功能证明终止的某一类循环。然后，我们提出了一个扩展的方法来显示存在的最终线性排名功能，即，线性函数，在循环的有限展开之后成为排名函数。证明了算法的正确性和完备性。
2013-06-08 cs.PL
Neural Termination Analysis
University of Birmingham（伯明翰大学）；Amazon, Inc.（亚马逊公司）；University of Oxford（牛津大学）
我们介绍了一种新的方法来自动终止分析的计算机程序：我们使用神经网络来表示排名功能。排名函数将程序状态映射到从下到上有界的值，并随着程序的运行而减少;排名函数的存在证明程序终止。我们训练一个神经网络从采样的执行轨迹的程序，使网络的输出沿轨迹减少，然后，我们使用符号推理正式验证，它概括到所有可能的执行。在肯定的答案，我们获得一个正式的证书终止程序，我们称之为神经排名功能。我们证明，由于神经网络的能力，代表非线性函数，我们的方法成功的程序，是超出了国家的最先进的工具。这包括在循环条件中使用析取的程序和包含非线性表达式的程序。
2022-09-06 cs.LG cs.LO cs.PL
A New Proof Rule for Almost-Sure Termination
概率程序的一个重要问题是它所有发散运行的概率质量是否为零，也就是说它“几乎必然”终止。证明这一点可能很难，本文提出了一种新的方法来做到这一点;它是在程序逻辑中表达的，因此直接适用于源代码。程序可能包含概率选择和恶魔选择，概率选择可能取决于当前状态。和其他研究人员一样，我们使用变量函数（也称为变量函数）。“超鞅”）是实值的，并且在每次循环迭代中概率可能会减少;但我们的关键创新在于减少的数量和概率是参数的。我们证明了新的规则的合理性，表明其适用性超出现有的规则，并解释其连接到经典的结果可数（非恶魔）马尔可夫链。
2017-12-26 cs.LO cs.PL
Termination Analysis Without the Tears
确定一个给定的程序是否终止是典型的不可判定问题。终止分析的算法分为两组：（1）具有强行为保证的算法，在有限的情况下工作（例如，多面体环的线性排序函数的完全综合[Podelski和Rybalchenko，2004]），以及（2）广泛适用，但具有弱行为保证的算法（例如，终结者[Cook等人，2006]）。本文探讨了这两者之间的空间：我们如何设计实用的终止分析与有用的行为保证？本文提出了一种终止分析，这是组合（分析一个复合程序的结果是其组件的分析结果的函数）和单调（“更多的信息进入分析产生更多的信息”）。该文件有两个主要贡献。第一个是一个扩展的Tarjan的方法解决路径问题的图解决无限路径问题。这为构建成分终止分析提供了基础。第二个是基于这个框架的单调条件终止分析的集合。我们证明了我们的工具CompACT（条件终止的成分和可预测分析）与最先进的终止工具相比具有竞争力，同时提供更强的行为保证。
2021-09-15 cs.PL
Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs
本文提出了一个wp风格的演算获得的概率程序的期望运行时间的界限。它的应用包括确定（可能无限）的期望终止时间的概率程序和证明积极的几乎必然终止-一个程序终止概率1在有限的期望时间？我们提供了几个证明规则的运行时间的循环，并证明了一个简单的操作模型的方法的可靠性。我们表明，我们的方法是一个保守的扩展Nielson的方法推理确定性程序的运行时。我们分析了一些示例程序的预期运行时间，包括一维随机游走和优惠券收集器问题。
2017-11-28 cs.LO cs.PL
Automatic Termination Analysis of Programs Containing Arithmetic Predicates
对于带有算术谓词的逻辑程序，显示终止并不容易，因为整数的通常顺序并没有充分的根据。一种新的方法，很容易纳入TermiLog系统的自动终止分析，在这种情况下，显示终止。该方法包括以下步骤：首先，自动推导出表示整数值域的有限抽象域。在此基础上，对程序进行抽象解释.其结果是一个有限数量的原子抽象的答案查询，用于扩展查询映射对的技术。对于每个潜在非终止的查询映射对，猜测有界（整数值）终止函数。如果遍历该对减少了终止函数的值，则建立终止。简单的函数通常足以满足每个查询映射对，这使我们的方法比传统方法更有优势，传统方法对所有循环使用单个终止函数，这必然会更复杂，更难自动猜测。值得注意的是，McCarthy的91函数的终止可以使用我们的方法自动显示。总之，所提出的方法是基于结合的查询映射对的技术的整数的有限抽象，并且基本上是能够划分为几种情况下，这样一个简单的终止功能足以为每种情况下的终止证明。因此，证明终止的整个过程可以在TermiLog和类似系统的框架内自动完成。
2000-11-23 cs.PL
Inference of Field-Sensitive Reachability and Cyclicity
在基于堆的语言中，知道变量x指向非循环数据结构对于分析终止是有用的：这个信息保证x指向的数据结构的深度大于x.fld指向的结构的深度，并且允许限制遍历fld上的数据结构的循环的迭代次数。一般来说，证明终止需要非循环性，除非执行程序特定的或非自动推理。然而，最近的工作可以证明，某些循环终止，甚至没有推断非循环，因为他们遍历数据结构“非循环”。考虑一个双向链表：如果可以证明每个循环都涉及“下一个”和“上一个”字段，则对“下一个”的遍历终止，因为没有循环将被完全遍历。本文提出了一种静态分析方法来推断场敏感的可达性和周期性信息，这比现有的方法更普遍。命题公式被计算，它描述了哪些字段可以或不可以被堆中的路径遍历。考虑一棵树，其边“左”和“右”分别是左子树和右子树，“父”是父结点：最先进的分析无法保证遍历叶子向上的循环的终止。相反，通过这种分析计算的命题公式表明，循环必须遍历“父”和“左”与“右”之间的至少一个：终止是保证的，因为没有循环被完全遍历。本文定义了必要的抽象域，并在其上建立了抽象语义。原型实现提供了相关示例的预期结果。
2014-05-19 cs.PL
How to Design While Loops
初学者发现被称为while循环的句法结构很难掌握。困难围绕着保证循环终止和学习如何正确地排序突变来解决问题。事实上，这两者是交织在一起的，学生需要学习一个模型，帮助他们推理如何设计while循环。对于已经介绍了如何使用结构递归，生成递归，累积递归和突变设计程序的学生，教他们如何设计while循环的任务变得更容易。例如，这些学生熟悉状态变量、终止参数和累加器不变量。所有这些都是while循环设计的基础。本文介绍了Seton Hall大学使用的一种新技术，向初学者介绍while循环的设计。它提出了一个设计食谱，学生可以按照一步一步地建立这样的事情，如循环的驱动程序，循环不变，和正确的突变序列。本文还提供了一个使用新设计配方设计基于while循环的函数的示例。
2020-08-21 cs.OH cs.PL
On Termination of Polynomial Programs with Equality Conditions
研究了一类多路多项式规划的终止问题，其中对程序变量的所有赋值都是多项式，循环和条件语句的测试条件都是多项式等式.我们表明，这样的程序的非终止输入（NTI）的集合是算法可计算的，从而导致其终止的可判定性。据我们所知，所考虑的MPP家族是迄今为止可决定终止的最大家族。本文给出了一个显式的递归函数，它本质上是阿克曼的，用来计算多项式理想在控制函数下的升链的最大长度，从而得到了Seidenberg问题的完整答案.这个最大的长度有利于我们的算法计算NTI和决定终止MPP的精确的复杂性分析。我们扩展我们的方法与多项式守护命令的程序，并显示如何不完整的程序与不等式警卫的MPP可以得到。我们的技术的多项式程序的不变生成的应用。
2020-09-01 cs.PL cs.SC
On Applying Or-Parallelism and Tabling to Logic Programs
在过去的几年里，人们在增加Prolog的声明性和表达性方面做出了越来越大的努力。表已被证明是一种可行的技术，有效地克服SLD的无限循环和冗余的子计算的敏感性。我们的研究表明，隐式或并行是一个自然的适合逻辑程序与制表。为了证实这一信念，我们已经设计并实现了一个或并行制表引擎- OPTYap -我们使用共享内存并行机来评估其性能。据我们所知，OPTYap是逻辑编程系统的并行制表引擎的第一个实现。OPTYap建立在Yap高效的顺序Prolog引擎之上。它的执行模型是基于SLG-WAM的制表，和环境复制或并行。初步结果表明，提出的机制，并行搜索的上下文中的SLD决议确实可以有效地和自然地推广到并行表计算，并由此产生的系统可以实现良好的性能共享内存并行机。更重要的是，它强调了我们的信念，通过应用或并行和制表逻辑程序的应用范围可以增加逻辑程序设计。
2003-08-04 cs.PL
Positive Supercompilation for a Higher-Order Call-By-Value Language
以前的森林砍伐和超级编译算法在应用于按值调用程序时可能会引入意外终止。这对程序员隐藏了循环错误，并根据程序是否优化来改变程序的行为。我们提出了一个高阶按值调用语言的超编译算法，并证明了该算法既终止，并保持终止属性。该算法利用严格性信息来决定是否替换，并与以前的按名称调用转换进行了比较。
2010-08-18 cs.PL
An Effective Quantum Hoare Logic for Hybrid Quantum Programs with Unbounded Loops
CEA LIST/LSL, Qbricks Team（CEA LIST/LSL，Qbricks团队）；Université de Lorraine, CNRS, Inria, LORIA, MOCQUA team（洛林大学、法国国家科学研究中心、法国国家信息与自动化研究所、洛林研究与教学实验室，MOCQUA团队）
针对混合量子程序中无界循环带来的分析挑战，引入整数混合路径和，提出基于循环不变量确定终止与资源消耗的策略，实现半自动Haskell程序，为设计完整静态资源分析工具迈出第一步。
2026-07-10 cs.PL quant-ph
Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops (Extended Version)
RWTH Aachen University（亚琛工业大学）；University College London（伦敦大学学院）；Cornell University（康奈尔大学）；Saarland University（萨尔兰大学）
本文提出了一种基于生成函数的自动方法，用于合成概率循环的占用不变量，以实现数学精确的推断。
2026-01-20 cs.PL
Invariant Generation for Multi-Path Loops with Polynomial Assignments
程序分析需要生成程序属性，这些属性表示在中间程序位置保持的条件。当涉及到具有循环的程序时，这些属性通常表示为循环不变式。在本文中，我们研究了一类多路径程序循环与数值变量，特别是嵌套循环的条件，其中的分配程序变量是多项式表达式的程序变量。我们称这类循环扩展P-可解的，并介绍了一种算法，用于生成所有的多项式不变量，这样的循环。通过一个迭代过程，采用格罗布纳基计算，我们的方法计算的多项式理想的多项式不变量的每个程序路径，并结合这些理想顺序，直到达到一个固定点。这个不动点表示给定的扩展P-可解循环的所有多项式不变量的多项式理想。我们证明了我们的方法的终止，并表明达到不动点的最大迭代次数线性依赖于程序变量的数量和内部循环的数量。特别地，对于一个有m个程序变量和r个条件分支的循环，我们证明了m*r次迭代的上界。我们在Alignator软件包中实现了我们的方法。此外，我们评估了18个程序与多项式运算，并比较它与现有的方法在不变量生成。结果表明，我们的方法的效率。
2018-01-11 cs.PL cs.SC
