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

【Abstract】 By inferring logic,this extending invariant an automatic verification system for C programs The based on shape graph paper proposes a method for loop shape graphs for binary tree programs.programs in difference between the proposed method and the method for inferring loop binary invariant shape graphs that for singly-linked list is the addition of some equivalence rules and implication rules designed shape,so tree for folding and paper makes unfolding designs uncertain algorithm for directions for can be when performed to during the the procedure of inferring loop-invariant addition,the shape graphs.tree graph.The In the deciding apply new rules while inferring loop-invariant shape binary proposed method it possible the verification system to automatically infer loop-invariant shape graphs for programs.更多还原