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

来源：软件学报杂志2017年第5期北京时间：

作者：翟娟,汤震浩,李彬,赵建华,李宣东

单位：翟娟，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023;南京大学 软件学院, 江苏 南京 21002311,汤震浩，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023;南京大学 计算机科学与技术系, 江苏 南京 21002302,李彬，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023;南京大学 计算机科学与技术系, 江苏 南京 21002303,赵建华，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023;南京大学 计算机科学与技术系, 江苏 南京 21002304,李宣东，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023;南京大学 计算机科学与技术系, 江苏 南京 21002305

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

关键词：循环摘要;循环不变式;前置条件;后置条件;程序验证

基金资助：国家自然科学基金（61632015，61561146394）；国家重点研发计划（2016YFB1000802）