计算最终线性秩函数的新方法

摘要

程序的终止性分析作为程序验证中重要的一环,在软件正确性验证中极为重要.对于一个线性循环程序,若该程序没有传统定义的线性秩函数,则基于传统定义的秩函数终止性分析方法失效.2013年,Bagnara提出了最终线性秩函数(Eventual Linear Ranking Functions)的定义,并证明了若某个程序存在最终线性秩函数,则该程序终止.由此,提出了新的方法来计算最终线性秩函数,构造了存在线性增函数和最终线性秩函数的等价半代数系统,并使用Mathematica工具对半代数系统进行求解,对比分析了各种最终秩函数求解方法的实际计算时间,结果证实了所提方法的优越性.%Termination of linear loop programs has received extensive attention in these years.In this paper,we focused on the termination of linear constraint loops which has no traditional linear ranking functions.A method of detecting eventual linear ranking functions by Bagnara were introduced for termination analysis first.Such an eventual linear ranking function implies the loop terminates.We presented a new method for computing eventual linear ranking functions.Semi-algebraic systems,equivalent to linear increasing functions and eventual linear ranking functions,were established.Several methods for synthesizing eventual linear ranking functions were compared.And experimental results show that the semi-algebraic system for synthesis of eventual linear ranking functions established by our method is simpler.