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

New Method for Computing Eventual Linear Ranking Functions

作　　者：朱广[1] 李轶[1] 吴文渊[1] ZHU Guang LI Yi WU Wen-yuan(Chongqing Institute of Green and Intelligent Technology, Chinese Academy of Sciences, Chongqing 400714, China)

机构地区：[1]中国科学院重庆绿色智能技术研究院,重庆400714

出　　处：《计算机科学》2017年第1期194-198,213,共6页Computer Science

基　　金：国家自然科学基金(61572024;11471307);重庆市基础与前沿研究计划院士专项(cstc2015jcyjys40001)资助

摘　　要：程序的终止性分析作为程序验证中重要的一环,在软件正确性验证中极为重要。对于一个线性循环程序,若该程序没有传统定义的线性秩函数,则基于传统定义的秩函数终止性分析方法失效。2013年,Bagnara提出了最终线性秩函数(Eventual Linear Ranking Functions)的定义,并证明了若某个程序存在最终线性秩函数,则该程序终止。由此,提出了新的方法来计算最终线性秩函数,构造了存在线性增函数和最终线性秩函数的等价半代数系统,并使用Mathematica工具对半代数系统进行求解,对比分析了各种最终秩函数求解方法的实际计算时间,结果证实了所提方法的优越性。Termination of linear loop programs has received on the termination of linear constraint loops which has no extensive attention in these years. In this paper, we focused 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 func- tions. Semi-algebraic systems, equivalent to linear increasing functions and eventual linear ranking functions, were estab- lished. 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.

关 键 词：线性循环程序 终止性分析 最终线性秩函数 MATHEMATICA 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]