首页 | 本学科首页   官方微博 | 高级检索  
     

计算最终线性秩函数的新方法
引用本文:朱广,李轶,吴文渊.计算最终线性秩函数的新方法[J].计算机科学,2017,44(1):194-198, 213.
作者姓名:朱广  李轶  吴文渊
作者单位:中国科学院重庆绿色智能技术研究院 重庆400714,中国科学院重庆绿色智能技术研究院 重庆400714,中国科学院重庆绿色智能技术研究院 重庆400714
基金项目:本文受国家自然科学基金(61572024,11471307),重庆市基础与前沿研究计划院士专项(cstc2015jcyjys40001)资助
摘    要:程序的终止性分析作为程序验证中重要的一环,在软件正确性验证中极为重要。对于一个线性循环程序,若该程序没有传统定义的线性秩函数,则基于传统定义的秩函数终止性分析方法失效。2013年,Bagnara提出了最终线性秩函数(Eventual Linear Ranking Functions)的定义,并证明了若某个程序存在最终线性秩函数,则该程序终止。由此,提出了新的方法来计算最终线性秩函数,构造了存在线性增函数和最终线性秩函数的等价半代数系统,并使用Mathematica工具对半代数系统进行求解,对比分析了各种最终秩函数求解方法的实际计算时间,结果证实了所提方法的优越性。

关 键 词:线性循环程序  终止性分析  最终线性秩函数  Mathematica
收稿时间:2015/12/16 0:00:00
修稿时间:2016/5/24 0:00:00

New Method for Computing Eventual Linear Ranking Functions
ZHU Guang,LI Yi and WU Wen-yuan.New Method for Computing Eventual Linear Ranking Functions[J].Computer Science,2017,44(1):194-198, 213.
Authors:ZHU Guang  LI Yi and WU Wen-yuan
Affiliation:Chongqing Institute of Green and Intelligent Technology,Chinese Academy of Sciences,Chongqing 400714,China,Chongqing Institute of Green and Intelligent Technology,Chinese Academy of Sciences,Chongqing 400714,China and Chongqing Institute of Green and Intelligent Technology,Chinese Academy of Sciences,Chongqing 400714,China
Abstract: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.
Keywords:Linear loop programs  Termination analysis  Eventual linear ranking functions  Mathematica
点击此处可从《计算机科学》下载全文
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号