S-程序演算

本文提出了一阶谓词逻辑的一个特殊子集，称为S-程序演算（简称S-演算）。S-演算是由所谓S-公式构成的演算，这些S-公式定义在虚拟机的抽象状态空间上。我们证明，S-公式是分析程序语义的极其通用的工具，因为完全正确性与部分正确性的Hoare三元组不过是两个S-公式。此外，使用S-公式以及一阶谓词演算的公理/定理，可以推导出Hoare逻辑的所有规则。S-演算是证明程序正确性以及利用谓词逻辑定理构建额外证明工具的强大机制。每个证明都基于推导某个S-公式的有效性，因此该过程可以使用自动定理证明器实现自动化（本文将使用Coq）。作为S-演算应用的示例，我们将证明Dijkstra算子wp的四个基本性质。Dijkstra给出的证明并未完全形式化，我们将展示使用S-演算可以实现完全形式化。最后，我们在上述四个性质之外再添加一个定理，即否定律。