一种用于指针程序验证的指针逻辑

本文改进并扩展先前为验证指针程序提出的指针逻辑,主要贡献是提出了合法访问路径集合的概念,极大地简化了访问路径上的基本运算,并使得指针逻辑推理规则变得易理解.另外,增加了局部推理规则和函数构造的推理规则,使得指针逻辑可以方便地用于有函数调用的场合.

Pointer Logic for Verification of Pointer Programs

This paper improves and extends the pointer logic that has been designed for verifying pointer programs. Its main contribution is that a concept of legal sets of access paths is presented, which simplifies elementary operations on access paths and makes inference rules of the logic easier to understand. Furthermore, the logic with inference rules is extended for local reasoning and for function construction, making the logic used conveniently in the context of function calls.