软件学报

作者：李轶，唐桐

单位：李轶，中国科学院 重庆绿色智能技术研究院 自动推理与认知中心, 重庆 40071411,唐桐，中国科学院 重庆绿色智能技术研究院 自动推理与认知中心, 重庆 400714;中国科学院大学, 北京 10004902

关键词：循环程序;线性秩函数;增函数;终止性;多阶段秩函数

基金：重庆市自然科学基金(cstc2019jcyj-msxmX0638);国家自然科学基金(11771421);中国科学院“西部之光”人才培养计划

秩函数法是循环终止性分析的主要方法,秩函数的存在表明了循环程序是可终止的.针对单分支线性约束循环程序,提出一种方法对此类循环的终止性进行分析.基于增函数法向空间的计算,该方法将原程序空间上的秩函数计算问题归结为其子空间上的秩函数计算问题.实验结果表明,该方法能有效验证现有文献中大部分循环程序的终止性.

来源：2024年第3期

《软件学报》期刊编辑部

查看软件学报杂志2024年第3期