用Dixon结式产生非线性循环不变式  

Non-linear Loop Invariant Generation Using Dxion Resultant

作　　者：余伟[1] 冯勇[1] 

机构地区：[1]中国科学院成都计算机应用研究所,四川成都610041

出　　处：《四川大学学报（工程科学版）》2012年第4期115-121,共7页Journal of Sichuan University (Engineering Science Edition)

基　　金：国家"973"计划资助项目(2011CB302402);国家自然科学基金面上项目(11171053);国家自然科学基金重大研究计划资助项目(91118001)

摘　　要：针对循环程序的部分正确性问题,在代数变迁系统理论基础上,结合约束理论提出了一种用Dixon结式生成循环不变式的算法。首先,程序被转换成代数变迁系统,再根据代数变迁关系和不变式模板构造一个多项式组,计算此多项式组的Dixon结式可以得到关于模板变量的约束,最后对该约束系统求解就得到该模板形式的程序不变式。经实例分析,该算法应用于单路径和多路径程序均是有效的。TO solve the partial correct problem of loop program, an algorithm was presented to generate non-linear loop invariant by computing Dixon resultant based on algebraic transition system and constraint system. The loop program was firstly transformed to an al- gebraic transition system, then a polynomial set was constructed from algebraic transition relation and invariant template, and a con- straint system w. r. t template variable was obtained by computing Dixon resultant. Finally the constraint system was resolved to get in- variant. The algorithm was effective to whether single-path or multi-path programs through case study.

关 键 词：循环不变式 Dixon结式 模板 约束 

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