李 轶, 蔡天训, 樊建峰,3, 吴文渊, 冯 勇

1(中国科学院 重庆绿色智能技术研究院 自动推理与认知重庆市重点实验室,重庆 400714)

2(萨基姆通讯(深圳)有限公司,广东 深圳 518000)

3(中国科学院大学 计算机科学与技术学院,北京 100093)

循环程序的终止性分析是程序验证的一个重要研究分支.在现代程序设计中,几乎所有的程序都会含有循环.然而,即使是简单的循环程序,也很容易出错.循环中的很多错误往往需要执行多次或在某些特定情况下才能被发现.因此,确保循环程序是可终止的是保障软件能够可靠运行的一个必要条件.尽管程序终止性问题早已被证明是一个不可判定问题[1,2].但是人们发现,具有某些特征的循环程序的终止性是可判定的.如:Tiwari在2004年证明了一类线性循环程序在实数域上的终止性是可判定[3].这类程序的终止性在文献[4-7]中被重新考虑.此外,Zhan等人在文献[8]中考虑了循环条件为等式的多项式程序的终止性问题,并给出了该类程序可终止和不可终止的充分判准.在文献[9]中,Zhang等人建立了针对程序终止性验证的高级自动机算法.在循环非终止研究方面,Zhang给出了一种能够检测出简单循环中出现死循环的充分条件[10].针对确定型线性赋值循环程序,Leike等人在文献[11]中给出了GNTA条件去探测这类循环的不可终止性.

秩函数法是证明循环程序可终止性的主要方法.给定一个循环程序,倘若它的秩函数被找到,则表明该循环是终止的.为计算秩函数……