| 基于k阶秩函数的线性赋值循环程序的终止性分析 |
| |
| 引用本文： | 李轶,蔡天训,吴文渊.基于k阶秩函数的线性赋值循环程序的终止性分析[J].计算机科学,2018,45(6):151-155. |
| |
| 作者姓名： | 李轶 蔡天训 吴文渊 |
| |
| 作者单位： | 重庆邮电大学计算机科学与技术学院 重庆400065;中国科学院重庆绿色智能技术研究院自动推理与认知重庆市重点实验室 重庆400714,重庆邮电大学计算机科学与技术学院 重庆400065;中国科学院重庆绿色智能技术研究院自动推理与认知重庆市重点实验室 重庆400714,中国科学院重庆绿色智能技术研究院自动推理与认知重庆市重点实验室 重庆400714 |
| |
| 基金项目： | 本文受国家自然科学基金(61572024,0,11471307)资助 |
| |
| 摘 要： | 循环程序的终止性是确保循环程序完全正确的必要条件。 如果给定的线性赋值循环程序不存在传统定义的线性秩函数,那么基于传统定义的秩函数终止性证明方法将失效。基于Anx的精确计算,对传统的秩函数概念进行了扩展,提出了k阶秩函数的概念。使用RegularChains软件包给出了合成k阶秩函数的具体方法。实验结果表明,相比于传统定义的线性秩函数,k阶秩函数的适应范围更广。对于 不能用传统定义的秩函数证明其终止性的部分循环程序,可以基于k阶秩函数来证明,从而体现了所提方法的优越性。
|
| 关 键 词： | 线性循环程序 终止性分析 k阶秩函数 RegularChains |
| 收稿时间： | 2017/4/26 0:00:00 |
| 修稿时间： | 2017/6/7 0:00:00 |
Termination Analysis of Linear Assignment Loop Program Based on k-ranking Functions |
| |
| LI Yi,CAI Tian-xun and WU Wen-yuan.Termination Analysis of Linear Assignment Loop Program Based on k-ranking Functions[J].Computer Science,2018,45(6):151-155. |
| |
| Authors: | LI Yi CAI Tian-xun and WU Wen-yuan |
| |
| Affiliation: | College of Computer Science and Technology,Chongqing University of Posts and Telecommunications,Chongqing 400065,China;Chongqing Key Laboratory of Automated Reasoning and Cognition,Chongqing Institute of Green and Intelligent Technology, Chinese Academy of Sciences,Chongqing 400714,China,College of Computer Science and Technology,Chongqing University of Posts and Telecommunications,Chongqing 400065,China;Chongqing Key Laboratory of Automated Reasoning and Cognition,Chongqing Institute of Green and Intelligent Technology, Chinese Academy of Sciences,Chongqing 400714,China and Chongqing Key Laboratory of Automated Reasoning and Cognition,Chongqing Institute of Green and Intelligent Technology, Chinese Academy of Sciences,Chongqing 400714,China |
| |
| Abstract: | The termination of loop programs plays an important role in program analysis.This paper focused on the termination of linear assignment loop programs which have no traditional linear ranking functions.Based on the precise computation of Anx,this paper expanded the concept of traditionally defined raking functions,gave a definition of k-ranking functions and proved the existence of k-ranking functions.All the computations on the synthesis of k-ranking functions were done by Regularchains,a symbolic computation tool in Maple.Experimental results show that some linearloop programs which have no traditional linear ranking functions indeed can be proven to be terminating by the proposed method. |
| |
| Keywords: | Linear loop programs Termination analysis k-ranking functions RegularChains |
|
|
点击此处可从《计算机科学》下载全文 |
|
