基于不变式生成的循环停机性验证

J4 ›› 2012, Vol. 34 ›› Issue (4): 108-113.

基于不变式生成的循环停机性验证

邢建英，李梦君，李舟军

（国防科学技术大学计算机学院，湖南长沙 410073）

收稿日期:2011-11-05 修回日期:2012-02-10 出版日期:2012-04-26 发布日期:2012-04-25
基金资助:
国家自然科学基金资助项目（60703075,60973105,90718017）；国家教育部博士点基金资助项目（20070006055）

A Proving the Termination of Loops Based on the Generation of Invariants

XING Jianying，LI Mengjun，LI Zhoujun

（School of Computer Science,National University of Defense Technology,Changsha 410073,China）

Received:2011-11-05 Revised:2012-02-10 Online:2012-04-26 Published:2012-04-25

摘要/Abstract

摘要：

循环的停机性验证是程序验证中的一个难点。程序不变式用来描述程序变量的取值关系，其中线性不变式可以帮助描述程序变量间的线性关系，循环不变式能够有效刻画循环中的变量关系。本文基于线性不变式和多项式循环不变式的生成，将循环的停机性验证转化为求解一个最优化问题，给出了一个实用的程序停机性验证框架。基于该框架可以自动地验证程序的停机性，并给出循环的复杂度上界。实验结果说明了该方法的实用性。

关键词: 不变式；停机性验证；最优化问题；复杂度上界

Abstract:

Proving the termination of loops is a difficult part of program verification. Program invariants 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 solving 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

邢建英，李梦君，李舟军. 基于不变式生成的循环停机性验证[J]. J4, 2012, 34(4): 108-113.

XING Jianying，LI Mengjun，LI Zhoujun. A Proving the Termination of Loops Based on the Generation of Invariants[J]. J4, 2012, 34(4): 108-113.