李轶,蔡天训,吴文渊.基于k阶秩函数的线性赋值循环程序的终止性分析[J].计算机科学,2018,45(6):151-155
基于k阶秩函数的线性赋值循环程序的终止性分析
Termination Analysis of Linear Assignment Loop Program Based on k-ranking Functions
投稿时间:2017-04-26  修订日期:2017-06-07
DOI:10.11896/j.issn.1002-137X.2018.06.026
中文关键词:  线性循环程序,终止性分析,k阶秩函数,RegularChains
英文关键词:Linear loop programs,Termination analysis,k-ranking functions,RegularChains
基金项目:本文受国家自然科学基金(61572024,0,11471307)资助
作者单位
李轶 重庆邮电大学计算机科学与技术学院 重庆400065
中国科学院重庆绿色智能技术研究院自动推理与认知重庆市重点实验室 重庆400714 
蔡天训 重庆邮电大学计算机科学与技术学院 重庆400065
中国科学院重庆绿色智能技术研究院自动推理与认知重庆市重点实验室 重庆400714 
吴文渊 中国科学院重庆绿色智能技术研究院自动推理与认知重庆市重点实验室 重庆400714 
摘要点击次数: 251
全文下载次数: 190
中文摘要:
      循环程序的终止性是确保循环程序完全正确的必要条件。 如果给定的线性赋值循环程序不存在传统定义的线性秩函数,那么基于传统定义的秩函数终止性证明方法将失效。基于Anx的精确计算,对传统的秩函数概念进行了扩展,提出了k阶秩函数的概念。使用RegularChains软件包给出了合成k阶秩函数的具体方法。实验结果表明,相比于传统定义的线性秩函数,k阶秩函数的适应范围更广。对于 不能用传统定义的秩函数证明其终止性的部分循环程序,可以基于k阶秩函数来证明,从而体现了所提方法的优越性。
英文摘要:
      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.
查看全文  查看/发表评论  下载PDF阅读器