CN43-1258/TP ISSN1007-130X
计算机工程与科学
COMPUTERENGINEERING&SCIENCE
文章编号：1007-130X(2012)04-0108-06
2012年第34卷第4期 Vol. 34,No. 4,2012
基于不变式生成的循环停机性验证 A Proving the Termination of Loops Based on the Generation of Invariants
邢建英，李梦君，李舟军
XING Jian-ying,LI Meng-jun,LI Zhou-jun
(国防科学技术大学计算机学院，湖南长沙410073)
(School of Computer Science,National University of Defense Technology,Changsha 410073,China)
要：循环的停机性验证是程序验证中的一个难点。程序不变式用来摘述程序变量的取值关系，其摘
中线性不变式可以帮助描迷程序变量间的线性关系，循环不变式能够有效刻画循环中的变量关系。本文基于线性不变式和多项式循环不变式的生成，将循环的停机性验证转化为求解一个最优化题，给出了一个实用的程序停机性验证框架。基于该柜架可以自动地验证程序的停机性，并给出循环的复杂度上界。实验结果说明了该方法的实用性。
Abstract:Proving the termination of loops is a difficult part of program verification.Program invari-ants can describe the relations of program variables, Linear invariants can describe the linear relations of variables, and the relations of variables in the loops can be presented by loop invariants, By generating linear invariants and polynomial loop invariants, we transform proving the termination of loops to sol-ving an optimization problem, then we present a practical framework of proving termination, Using the framework, the termination of loops can be proved automatically, and the complexity bounds of loops can be computed. The experimental results show the practicality of the method.
关键词：不变式；停机性验证；最优化问题；复杂度上界
Key words:invariant:proving termination;optimization problem;complexity bound doi:10.3969/j.issn. 1007-130X.2012.04.021
中图分类号：TP301
1
引言
停机性验证是程序验证的重要组成部分。完
全正确的程序必须停机，但对于象"whileb(S)"这样简单的循环米说，证明它的停机性也不是很容易。理论上，程序的停机性证明是一个不可判定性问题，即使循环中所有循环条件和循环体中所有赋值语句都是线性形式，它的停机性间题仍然是不可判定性的"。对于存在多路径和循环嵌套的循环程序，验证它们的停机性更加困难。
文献标识码：A
对于程序的停机性问题，学者们已经开展了大量的研究工作。强制式线性程序的停机性研究主要采用线性秩函数方法，线性秩函数是循环变量和常数的线性组合，其值域是一个良基集，并且它的取值随每次循环持续递减。Colon和Sipma在文献[2]中将线性秩函数引人到程序停机性证明工作中，在文献[3]中，Colon和Sipma基于凸多面体给出了线性秩函数的一种综合方法，并将其应用到多路径循环和嵌套循环的停机性验证。Podelski和 Rybalchenko在文献[4,5]中给出了线性秩函数的一种完备的综合方法，并证明了对于只含线性卫式
收稿日期：2010-10-08；修订日期：2011-03-12
基金项目：国家门热科学基金资助项日（60703075，60973105.90718017）：国家教育部博士点基金资助项目（20070006055）通讯地址：410073湖南省长沙市国防科学技术大学计算机学院学员七队
Address;School of Computer Science,Nationai University of Defense Technology,Changsha,Hunan 410073,P, R, China 万方数据