论文部分内容阅读
程序的终止性分析作为程序验证中重要的一环，在软件正确性验证中极为重要。对于一个线性循环程序，若该程序没有传统定义的线性秩函数，则基于传统定义的秩函数终止性分析方法失效。2013年，Bagnara提出了最终线性秩函数（Eventual Linear Ranking Functions）的定义，并证明了若某个程序存在最终线性秩函数，则该程序终止。由此，提出了新的方法来计算最终线性秩函数，构造了存在线性增函数和最终线性秩函数的等价半代数系统，并使用Mathematica工具对半代数系统进行求解，对比分析了各种最