形式陈述

公理语义用逻辑断言刻画程序行为。Hoare 三元组

$$ \{P\}\ C\ \{Q\} $$$$\{P\}C\{Q\}$$

在部分正确性语义下表示：任意满足前置条件 $P$$P$ 的初始状态，只要命令 $C$$C$ 终止，其终止状态就满足后置条件 $Q$$Q$。赋值公理为

$$ \{Q[e/x]\}\ x:=e\ \{Q\}, $$$$\{Q[e/x]\}x:=e\{Q\},$$

其中 $Q[e/x]$$Q[e/x]$ 是避免变量捕获的替换。顺序、条件与循环规则把局部断言组合起来；循环规则需要不变式 $I$$I$。

直觉

公理语义不逐步模拟程序，而是把程序当成状态转换器，询问某些性质在执行前后是否成立。证明程序正确性由此变成在逻辑系统中构造推导。

例子与边界

对命令 $x:=x+1$$x:=x+1$，三元组

$$ \{x=0\}\ x:=x+1\ \{x=1\} $$$$\{x=0\}x:=x+1\{x=1\}$$

可由赋值公理得到。三元组 $\{\mathrm{true}\}\texttt{while true do skip}\{Q\}$$\{\mathrm{true}\}\mathtt{\text{while true do skip}}\{Q\}$ 在部分正确性下对任意 $Q$$Q$ 都成立，因为程序没有终止状态；它不能证明终止。总正确性还需加入终止论证，如良基变式。

推论与应用

Hoare 逻辑用于程序验证、验证条件生成与循环不变式推导。可靠性说明可推导三元组在语义上有效；相对完备性则依赖断言语言能表达所需事实，不能理解为自动判定任意程序正确性。

参考资料

• Glynn Winskel, The Formal Semantics of Programming Languages, MIT Press, 1993，Chs. 6–7。
• C. A. R. Hoare, “An Axiomatic Basis for Computer Programming,” Communications of the ACM 12(10), 1969，Full paper, axioms and rules。