【摘要】 在一个基于形状图逻辑的自动程序验证原型系统上,设计与实现了指针类型递归函数前后形状图的自动推断方法.该方法类似于循环不变形状图的推断方法,区别在于它首先沿着函数的非递归路径,从函数入口的函数前形状图推断函数出口的函数后形状图的初值,然后沿着函数的递归路径对函数后形状图进行迭代求解.本文还设计了上述自动推断方法中需要用到的形状图之间蕴涵关系的判定方法.本文方法使得原型系统扩展到能够自动验证指针类型的递归函数.更多还原

【Abstract】 By extending an existing automatic program verification prototype system based on shape graph logic,this paper puts forward a method for inferring pre and post shape graphs for pointer-type recursive functions. While this method is similar to the inference method for loop-invariant shape graphs,it infers initial post shape graph at function’ s exit from its entrance’ s pre shape graph through non-recursive paths and then infers its post shape graph iteratively through recursive paths. Besides,the paper designs the decision method for implication between shape graphs used by the inferring method above. The paper makes it possible for the prototype system to automatically verify pointer-type recursive functions.更多还原