具有局部推理和前后状态属性的作用域逻辑

本文提出了对用于指针程序验证的 Hoare 逻辑的一种扩展。使用带有用户定义递归函数的逻辑公式来指定程序执行前后程序状态的属性。引入了三个基本函数来表示内存访问、记录字段访问和数组元素访问。在我们的逻辑中引入了一些公理来指定这些基本函数。在我们的逻辑中引入了内存作用域函数（MSF）的概念。给定一个递归函数 $f$，$f$ 的 MSF 计算在 $f$ 求值期间访问的内存单元集合。给出了一组规则，用于从 $f$ 的定义语法上推导出该 MSF 的定义。由于 MSF 也是递归函数，它们也有自己的 MSF。给出了一个公理来指定一个 MSF 包含其自身的 MSF。基于该公理，通过谓词变量支持局部推理。使用前状态项来指定前状态和后状态之间的关系。人们可以在后置条件中使用前状态项来表示前状态上的值。修改了 Hoare 逻辑中赋值语句的公理以处理指针。基本思想是，在程序执行期间，只要其内存作用域中的内存单元未被修改，递归函数就会被求值为相同的值。为内存分配语句添加了另一个证明规则。我们使用一个简单的例子来展示我们的逻辑可以处理指针程序。在附录中，使用我们的逻辑证明了 Shorre-Waite 算法。我们还使用选择排序程序来展示我们的逻辑可以用于证明具有间接指定组件的程序。