用daikon发现循环不变式

Discovering Loop Invariants Using Daikon

随着软件行业的深入发展,软件存在的问题与日俱增,程序正确性受到了广泛的关注,形式化方法是解决程序正确性的基本途径,而发现程序循环不变式是证明程序正确性的关键。本文介绍了循环不变式的基本概念以及计算不变式的基本方法;用JAVA重写了Siemens的replace C程序,并以JAVA和C两种语言的replace程序为例,对不变式动态探测工具daikon进行了深入的实验研究,试验结果揭示了daikon在探测循环语句不变式方面的不足,依此提出了改进daikon探测循环不变式的措施。

With the rapid development of software engineering, the correctness of programs becomes more and more important. The formalization method is a crucial approach to prove the correctness of programs whose key point is to discover the proper loop invariants. In the paper, the basic concepts and computational methods of loop invariants are briefly introduced. The Siemens replacing c program is rewritten in java that is used to test daikon with various cases. The experimental results shows that daikon has some intrinsicin drawbacks on discovering loop invariant. Accordingly, some potential improvements was proposed for daikon on purpose.