科研之友
微信
新浪微博
Facebook
分享链接
摘要
生成循环不变式是实现程序验证的关键步骤，但人工撰写循环不变式不仅步骤繁琐且容易出错。为此，提出一种基于数据分类的循环不变式生成方法，可直接为C程序的循环语句自动生成循环不变式。该方法生成循环程序的后置条件，并构造其Hoare三元组，通过收集循环程序执行过程中产生的测试数据，并根据其是否满足循环不变式的三个条件进行分类，从而生成循环不变式。所提出的方法在31个基准测试程序上，与目前比较先进的循环不变式生成方法进行比较分析。实验结果表明，所提出的方法不仅能够为C程序自动生成可验证的循环不变式，而且能够为最多的基准测试程序生成有效的循环不变式。
-
单位南京理工大学紫金学院; 南京大学
