公开(公告)号：CN106681786A

公开(公告)日：2017-05-17

申请号：CN201710005782.1

申请日：2017-01-05

申请人： 南京大学

发明人： 翟娟 ,  赵建华 ,  汤震浩 ,  李彬 ,  李宣东

IPC分类号： G06F9/45

CPC分类号： G06F8/42 ,  G06F8/436

摘要： 本发明的自动合成常用循环的摘要并生成程序规约的方法，包括步骤：1.生成待验证程序的抽象语法树；2.分析步骤1生成的抽象语法树来生成程序语句的摘要；3.对步骤2中生成的摘要进行分析生成程序语句的规约；4.对步骤3中生成的规约进行验证，从而辅助证明待验证程序的性质。本发明通过将操作常用数据结构的循环语句转换为一系列抽象的赋值语句，有效地对这类循环语句进行了抽象，使得可以使用赋值语句的分析方法来分析循环语句。本发明根据语句的摘要所生成的程序规约有效地描述了程序的性质，尤其是程序执行前后程序状态之间的关系，这些规约高效地辅助了程序的验证过程，提高程序验证的自动化程度和效率，减轻验证人员的负担。