中国科学院重庆绿色智能技术研究院机构知识库

QQ客服 官方微博 反馈留言

	基于k阶秩函数的线性赋值循环程序的终止性分析
	李轶1; 蔡天训1; 吴文渊2
	2018
摘要	循环程序的终止性是确保循环程序完全正确的必要条件。如果给定的线性赋值循环程序不存在传统定义的线性秩函数,那么基于传统定义的秩函数终止性证明方法将失效。基于Anx的精确计算,对传统的秩函数概念进行了扩展,提出了k阶秩函数的概念。使用RegularChains软件包给出了合成k阶秩函数的具体方法。实验结果表明,相比于传统定义的线性秩函数,k阶秩函数的适应范围更广。对于不能用传统定义的秩函数证明其终止性的部分循环程序,可以基于k阶秩函数来证明,从而体现了所提方法的优越性。
发表期刊	计算机科学
ISSN	1002-137X
卷号	045期号:006页码:151
收录类别	CSCD
CSCD记录号	CSCD:6259856
语种	英语