二叉树程序循环不变形状图的自动推断

• 作者: 李云龙 罗奇鸣 陈意云
• 来源期刊: 小型微型计算机系统
• 学科: 工学
• 关键词: 程序验证 形状图逻辑 形状分析 二叉树 循环不变形状图的自动推断
• 年，卷（期）: 2017,（5）
• 所属期刊栏目: 计算机软件与数据库研究
• 页码范围: 913-918
• 页数: 6页
• 分类号: TP311
• 字数: 8016字
• 语种: 中文

摘要

在一个基于形状图逻辑的C语言程序自动验证系统上,设计并实现了二叉树形状程序的循环不变形状图的自动推断方法.该方法与单链表程序循环不变形状图的推断方法的区别在于通过增加二叉树形状的等价和蕴含规则,使得在形状图的演算时支持二叉树中不确定方向的展开和折叠.此外,为了解决形状图变换规则变化给循环不变形状图推断带来的问题,还设计了算法用以判断在推断循环不变形状图的过程中是否使用新增的规则,并将判断算法融合到循环不变形状图推断流程中.本文方法使得系统支持自动推断二叉树指针程序的循环不变形状图.