非线性循环不变式的自动生成  

Automatic generation of non-linear loop invariants

作　　者：毕忠勤[1] 曾振柄[1] 郭远华[1] 

机构地区：[1]华东师范大学上海市高可信计算重点实验室,上海200062

出　　处：《计算机应用》2008年第7期1854-1857,共4页journal of Computer Applications

基　　金：国家自然科学基金资助项目(90718041);国家973计划项目(2004CB318003);国家863计划项目(2007AA010302);华东师范大学2008年优秀博士生培养基金资助项目(20080029)

摘　　要：提出了一个自动生成非线性循环不变式的算法。循环不变式可以表示成一个带参数的多项式的形式,根据断言的归纳特性,将循环不变式的生成问题转变成一个约束求解问题,这个约束求解问题的每个解对应于一个循环不变式,如果约束求解问题仅有零解,则说明不存在该参数多项式形式的循环不变式。该算法在Maple中得到了实现,并通过一些实例说明了该算法的有效性。This paper proposed an approach to automatically generate non-linear loop invariants. An invariant of a loop was hypothesized as a parameterized polynomial. Based on the inductive assertion＇s properties, we reduced the non-linear loop invariant problem to a numerical constraint solving problem. All the solutions to these constraints were the non-linear loop invariants of the program. The approach has been implemented in Maple. The implementation has been used to automatically discover nontrivial invariants for many programs.

关 键 词：程序验证 循环不变式 变迁系统 约束求解问题 

分 类 号：TP311.1[自动化与计算机技术—计算机软件与理论]