论文部分内容阅读
为类C小语言PointerC设计的指针逻辑，是Hoare逻辑的一种扩展，可用来对指针程序进行精确的指针分析，以支持指针相等关系确定的程序的安全性验证。本文扩展了这种指针逻辑，主要贡献是通过增加相等关系不确定的指针类型访问路径集合，使得指针逻辑可以应用于有向图等指针相等关系小确定的抽象数据结构上的指针程序性质证明。