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

• 作者: 李彬 汤震浩 翟娟 赵建华
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 霍尔式程序证明 程序分析 递归数据结构 归纳性质 过程间分析
• 年，卷（期）: 2018,（6）
• 所属期刊栏目: 形式化方法的理论基础专题
• 页码范围: 1527-1543
• 页数: 17页
• 分类号: TP311
• 字数: 15215字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.005467

摘要

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