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

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