.png){kind=icon}
返回
Algebraic and algorithmic methods for computing polynomial loop invariants
.png){kind=icon}
PRE
AI
DOI：10.1016/j.jsc.2025.102551.png)
.png){kind=icon}
原文求助.png){kind=icon}
分享.png){kind=icon}
收藏
摘要
En 中文
循环不变量是程序循环的性质，在循环的每次迭代之前和之后都成立。它们常用于验证程序，确保算法在执行过程中持续产生正确结果。因此，生成不变量成为循环的关键任务。我们特别关注多项式循环，其中循环条件和循环内的赋值均表示为多项式。尽管为一般循环计算多项式不变量是不可判定的，但已为某些类别的循环开发了高效算法。例如，当while循环内的所有赋值涉及线性多项式时，该循环变为可解的。在本工作中，我们研究更一般的情况，其中多项式可以具有任意次数。利用代数几何的工具，我们提出两种算法，旨在为具有非确定性条件语句的分枝循环生成给定向量子空间内的所有多项式不变量。这些算法结合线性代数子程序与多项式理想的计算。它们根据循环变量的初始值是否被指定或作为参数处理而有所不同。此外，我们还提出了一种更高效的算法，适用于特定形式的不变量，适用于所有初始值。该算法避免了昂贵的理想计算。(c) 2025 Elsevier Ltd. All rights are reserved, including those for text and data mining, AI training, and similar technologies.
Keyword:
Program synthesis
Loop invariants
Polynomial ideals
Symbolic algebraic computations
期刊
J
IF:
1.1
论文数:
38
被引数:
0
机构
引用论文
.png){kind=icon}
分享收藏Algebro-geometric Algorithms for Template-Based Synthesis of Polynomial Programs代数几何算法用于基于模板的多项式程序合成
PREAI
分享收藏
查看更多内容