作用域逻辑：面向指针程序验证的 Hoare 逻辑扩展

本文提出了 Hoare 逻辑的一种扩展，用于指针程序验证。首先，将 VDM 使用的偏函数逻辑（LPF）进行扩展，以使用指针和复合类型的内存布局来指定内存访问。然后，本文引入了数据检索函数（DRF）和内存作用域函数（MSF）的概念。人们可以定义 DRF 以从相互连接的具体数据对象中检索抽象值。DRF 对应的 MSF 的定义可以从 DRF 的定义中语法地推导出来。该 MSF 计算当 DRF 检索抽象值时所访问的内存单元集合。该内存单元集合被称为抽象值的内存作用域。最后，修改了 Hoare 逻辑中赋值语句的证明规则以处理指针。其基本思想是，只要其作用域内没有内存单元被覆写，一个虚拟值就保持不变。另外为内存分配语句增加了一条证明规则。推论规则和控制流语句的规则作了轻微修改，它们本质上与 Hoare 逻辑中的原始版本相同。本文给出了一个例子以展示该逻辑的有效性，并就如何验证指针程序提供了一些启发式方法。