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

摘要：

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

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

所属期刊栏目：29

分类号：TP311(计算技术、计算机技术)

资助基金：国家重点研发计划2016YFB1000802;国家自然科学基金61632015,61561146394National Key Research and Development Program of China2016YFB1000802;National Natural Science Foundation of China61632015,61561146394

在线出版日期：2018-07-12（万方平台首次上网日期，不代表论文的发表时间）

页数：共17页

页码：1527-1543