基于k阶秩函数的线性赋值循环程序的终止性分析

• 作者: 吴文渊 李轶 蔡天训
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: 线性循环程序 终止性分析 k阶秩函数 RegularChains
• 年，卷（期）: 2018,（6）
• 所属期刊栏目: 软件与数据库技术
• 页码范围: 151-155
• 页数: 5页
• 分类号: TP311.5
• 字数: 6933字
• 语种: 中文
• DOI: 10.11896/j.issn.1002-137X.2018.06.026

摘要

循环程序的终止性是确保循环程序完全正确的必要条件.如果给定的线性赋值循环程序不存在传统定义的线性秩函数,那么基于传统定义的秩函数终止性证明方法将失效.基于Anx的精确计算,对传统的秩函数概念进行了扩展,提出了k阶秩函数的概念.使用RegularChains软件包给出了合成k阶秩函数的具体方法.实验结果表明,相比于传统定义的线性秩函数,k阶秩函数的适应范围更广.对于不能用传统定义的秩函数证明其终止性的部分循环程序,可以基于k阶秩函数来证明,从而体现了所提方法的优越性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李轶	重庆邮电大学计算机科学与技术学院	13	20	2.0	4.0
3	吴文渊	中国科学院重庆绿色智能技术研究院自动推理与认知重庆市重点实验室	19	79	6.0	8.0
6	蔡天训	重庆邮电大学计算机科学与技术学院	1	0	0.0	0.0