文件名称：用Dixon结式产生非线性循环不变式 (2012年)
文件大小：427KB
文件格式：PDF
更新时间：2024-06-05 23:30:50
工程技术 论文
针对循环程序的部分正确性问题，在代数变迁系统理论基础上，结合约束理论提出了一种用Dixon结式生成循环不变式的算法。首先，程序被转换成代数变迁系统，再根据代数变迁关系和不变式模板构造一个多项式组，计算此多项式组的Dixon结式可以得到关于模板变量的约束，最后对该约束系统求解就得到该模板形式的程序不变式。经实例分析，该算法应用于单路径和多路径程序均是有效的。