自动分析递归数据结构的归纳性质

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

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

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

摘要：提出了一种对递归数据结构的归纳性质进行自动化分析的框架.工作分为3个主要部分.首先，它将递归数据结构的归纳性质分为两个主要类别，并提出对应的处理模式，从而帮助简化对于程序中的递归数据结构上的相关性质的分析.其次，提出了一种称为分割与拼接的技术来发现和描述递归数据结构是如何被程序修改的：递归数据结构首先被分割为若干个互不相交的片段，然后，这些片段以新的方式重新拼接在一起，形成一个新的数据结构.这个技术的重点在于如何将程序原有的性质保留下来，从而为后面的分析过程所使用.最后，提出了一种调用上下文敏感的程序摘要过程间分析方法.案例分析和实验结果表明：分析框架可以有效地分析递归数据结构的归纳性质，并生成对程序证明过程有用的断言.

关键词：霍尔式程序证明;程序分析;递归数据结构;归纳性质;过程间分析

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