常用循环摘要的自动生成方法及其应用

采用形式化方法证明软件的正确性是保障软件可靠性的有效方法，而对循环语句的分析与验证是形式化证明中的关键，对循环语句的处理一直是程序分析与验证中的一个难点问题.本文提出使用循环语句修改的内存和这些内存中存放的新值来描述循环语句的执行效果，并将该执行效果定义为循环摘要.同时，本文提出了一种自动生成循环摘要的方法，可以为操作常用数据结构的循环自动生成循环摘要，包含嵌套循环.此外，基于循环摘要，我们可以自动生成循环语句的规约，包括循环不变式、循环的前置条件以及循环的后置条件.我们已经实现了自动生成循环摘要以及循环规约的方法，并将它们集成到验证工具Accumulator中，实验表明，我们的方法可以有效地生成循环摘要，并生成多种类型的规约，从而辅助软件程序的形式化证明，提高验证的自动化程度和效率，减轻验证人员的负担.