| 单分支线性约束循环程序的终止性分析 |
| |
| 引用本文： | 李轶,唐桐.单分支线性约束循环程序的终止性分析[J].软件学报,2024,35(3):1307-1320. |
| |
| 作者姓名： | 李轶 唐桐 |
| |
| 作者单位： | 中国科学院 重庆绿色智能技术研究院 自动推理与认知中心, 重庆 400714;中国科学院 重庆绿色智能技术研究院 自动推理与认知中心, 重庆 400714;中国科学院大学, 北京 100049 |
| |
| 基金项目： | 重庆市自然科学基金(cstc2019jcyj-msxmX0638);国家自然科学基金(11771421);中国科学院“西部之光”人才培养计划 |
| |
| 摘 要： | 秩函数法是循环终止性分析的主要方法,秩函数的存在表明了循环程序是可终止的.针对单分支线性约束循环程序,提出一种方法对此类循环的终止性进行分析.基于增函数法向空间的计算,该方法将原程序空间上的秩函数计算问题归结为其子空间上的秩函数计算问题.实验结果表明,该方法能有效验证现有文献中大部分循环程序的终止性.
|
| 关 键 词： | 循环程序 线性秩函数 增函数 终止性 多阶段秩函数 |
| 收稿时间： | 2022/3/1 0:00:00 |
| 修稿时间： | 2022/5/1 0:00:00 |
Termination Analysis of Single-path Linear Constraint Loops |
| |
| LI Yi,TANG Tong.Termination Analysis of Single-path Linear Constraint Loops[J].Journal of Software,2024,35(3):1307-1320. |
| |
| Authors: | LI Yi TANG Tong |
| |
| Affiliation: | Automated Reasoning and Cognition Center, Chongqing Institute of Green and Intelligent Technology, Chinese Academy of Sciences, Chongqing 400714, China; Automated Reasoning and Cognition Center, Chongqing Institute of Green and Intelligent Technology, Chinese Academy of Sciences, Chongqing 400714, China;University of Chinese Academy of Sciences, Beijing 100049, China |
| |
| Abstract: | The ranking function method is the main method for the termination analysis of loops, and it indicates that loop programs can be terminated. In view of single-path linear constraint loop programs, this study presents a method to analyze the termination of the loops. Based on the calculation of the normal space of the increasing function, this method considers the calculation of the ranking function in the original program space as that in the subspace. Experimental results show that the method can effectively verify the termination of most loop programs in the existing literature. |
| |
| Keywords: | loop program linear ranking function increasing function termination multiphase ranking function |
|
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
