形式化2|霍尔逻辑

参考文献：

Hoare C A R. An axiomatic basis for computer programming[J]. Communications of the ACM, 1969, 12(10): 576-580. https://dl.acm.org/doi/10.1145/363235.363259

程序语义与霍尔逻辑

为什么对属性的验证可以转化为逻辑公式的可满足性？这两者真的等价吗？

对于一个可执行的C语言程序而言，比较直观的语义（Semantics）理解应该是，内存中有一部分存储着程序的二进制指令（Command），然后有一个指向当前执行指令的特殊指针变量（即程序计数器，Program Counter，pc），还有一部分存储着每个变量的值（栈和堆，Stack and Heap）。 随着程序指令的依次执行，内存的状态发生变化，比如赋值语句导致变量的值改变，控制流语句产生指令跳转，导致pc发生变化。 将这个过程形式化地定义出来，就是直观的操作语义（Operational Semantics）。 它定义了一个状态机（State Machine），将程序每一步执行所产生的影响，反应到状态机的状态变化上。

这样的程序语义和程序的实际运行情况非常切合，但却不利于逻辑和数学表达。 因此，在进行程序分析和验证时，我们会求诸于更加贴近于数学表达的公理语义（Axiomatic Semantics）。 霍尔逻辑（Floyd-Hoare Logic）便是一种典型的建立在谓词逻辑基础上的公理语义。 在其基础上，我们可以在程序代码和谓词逻辑公式之间，建立起「等语义关系」的转化，从而确保我们的程序验证方法是有效的。

霍尔三元组

霍尔逻辑核心概念是霍尔三元组，记为以下形式：

$$\{P\}c\{Q\}$$

其中$P$和$Q$是一阶逻辑公式。分别表示前置条件（pre-condition）和后置条件（post-condition）。$c$表示一段程序源代码。霍尔三元组的含义是，假定前置条件$P$是有效的，那么在执行完程序$c$后，后置条件$Q$将会是有效的。例如如下非形式化的霍尔三元组：

其中$\operatorname{gcd}(a, b)$是求$a$和$b$的最大公约数的函数。这个霍尔三元组说明，只要输入是两个正整数，那么就能计算出两者的最大公约数，即$\operatorname{gcd}(a, b)$函数实现的功能是正确的。

再来一个例子，交换两个数：

$$\begin{aligned} & \left\{x=x_0 \wedge y=y_0\right\} \\ & \mathrm{x}=\mathrm{x}+\mathrm{y} ; \mathrm{y}=\mathrm{x}-\mathrm{y} ; \mathrm{x}=\mathrm{x}-\mathrm{y} \\ & \left\{x=y_0 \wedge y=x_0\right\} \end{aligned}$$