形式陈述

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\},$$

顺序、条件和循环由组合规则处理；while 规则需要循环不变式 $I$$I$，证明初始化、保持和退出条件。总正确性还要额外证明终止，通常借良基变式量。

直觉

前置条件描述允许进入程序的状态，后置条件描述正常结束时必须达到的状态；三元组把程序看成状态关系上的逻辑契约。

例子与边界

$\{x=n\}\ x:=x+1\ \{x=n+1\}$$\{x=n\}x:=x+1\{x=n+1\}$ 有效。对 while true do skip，部分正确性三元组 $\{P\}C\{Q\}$$\{P\}C\{Q\}$ 对任意 $P,Q$$P,Q$ 都因程序不终止而真，这正说明它不含终止保证。循环不变式必须在每次迭代前后成立，但不必单独蕴含最终目标；还需结合退出条件。

推论与应用

Hoare 逻辑支撑演绎验证、契约、循环不变式生成和验证条件。可靠性证明把每条规则连接到程序语义；相对完备性则分析断言语言足够表达时还能证明哪些正确程序。

参考资料

• C. A. R. Hoare, “An Axiomatic Basis for Computer Programming,” Communications of the ACM 12(10), 1969，Full paper, axioms and rules for assignment, sequencing, conditionals, and loops。
• Edsger W. Dijkstra, A Discipline of Programming, Prentice Hall, 1976，Chs. 1–2, assertions and guarded commands。