基于k阶秩函数的线性赋值循环程序的终止性分析
文献类型：期刊论文
| 作者 | 李轶2 ; 蔡天训2; 吴文渊1
|
| 刊名 | 计算机科学
 |
| 出版日期 | 2018 |
| 卷号 | 045期号:006页码:151 |
| ISSN号 | 1002-137X |
| 英文摘要 | 循环程序的终止性是确保循环程序完全正确的必要条件。如果给定的线性赋值循环程序不存在传统定义的线性秩函数,那么基于传统定义的秩函数终止性证明方法将失效。基于Anx的精确计算,对传统的秩函数概念进行了扩展,提出了k阶秩函数的概念。使用RegularChains软件包给出了合成k阶秩函数的具体方法。实验结果表明,相比于传统定义的线性秩函数,k阶秩函数的适应范围更广。对于不能用传统定义的秩函数证明其终止性的部分循环程序,可以基于k阶秩函数来证明,从而体现了所提方法的优越性。 |
| 语种 | 英语 |
| 源URL | [http://119.78.100.138/handle/2HOD01W0/9440]  |
| 专题 | 自动推理与认知研究中心 |
| 作者单位 | 1.中国科学院重庆绿色智能技术研究院 2.重庆邮电大学 |
| 推荐引用方式 GB/T 7714 | 李轶,蔡天训,吴文渊. 基于k阶秩函数的线性赋值循环程序的终止性分析[J]. 计算机科学,2018,045(006):151. |
| APA | 李轶,蔡天训,&吴文渊.(2018).基于k阶秩函数的线性赋值循环程序的终止性分析.计算机科学,045(006),151. |
| MLA | 李轶,et al."基于k阶秩函数的线性赋值循环程序的终止性分析".计算机科学 045.006(2018):151. |
入库方式： OAI收割
来源：重庆绿色智能技术研究院
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。