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

摘要：

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

关键词：线性循环程序、终止性分析、k阶秩函数、RegularChains

所属期刊栏目：45

分类号：TP311.5(计算技术、计算机技术)

资助基金：国家自然科学基金61572024,61103110,11471307

在线出版日期：2018-08-30（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：151-155