霍尔逻辑

霍爾邏輯（英語：Hoare Logic），又稱弗洛伊德-霍爾邏輯（Floyd–Hoare logic），是英国计算机科学家東尼·霍爾开发的形式系统，这个系统的用途是为了使用严格的数理逻辑推理來替计算机程序的正确性提供一组逻辑规则。

這個想法起源於罗伯特·弗洛伊德於較早的研究，他为流程图提供了类似的系统。東尼·霍爾於1969年首次發表^[1]，随后为其他研究者所精制。

霍爾三元組

霍爾邏輯的中心特征是霍爾三元組（Hoare triple）。这种三元组描述一段代码的执行如何改变计算的状态。Hoare三元组有如下形式

${\displaystyle \{P\}\;C\;\{Q\}}$ 

这里的 P 和 Q 是 断言 而 C 是命令 。P 叫做 前条件 而 Q 叫做 后条件 。断言是谓词逻辑的公式。这个三元组在直觉上读做：只要 P 在 C 执行前的状态下成立，则在执行之后 Q 也成立。注意如果 C 不终止，也就没有"之后"了，所以 Q 在根本上可以是任何语句。实际上，你可以选择 Q 为假来表达 C 不终止。事實上，这種情形叫做 "部分正确（partial correctness）"。如果 C 终止并且在终止时 Q 是真，则表达式被稱作 "全部正确性（total correctness）"。终止必须被单独证明。

霍爾邏輯为简单的指令式编程语言的所有构造提供了公理和推理规则。除了给Hoare论文中的简单语言的规则，其他语言构造的规则也已经被Hoare和很多其他研究者开发完成。包括并发、过程、分支語句，和指针。

部分正确性

空语句公理

${\displaystyle {\frac {}{\{P\}\ {\textbf {skip}}\ \{P\}}}\!}$ 

如果P在一个空语句之前成立，那么在执行这个空语句之后也是成立的。 "skip"在这里表示空语句（Empty statement）。

赋值公理模式

赋值公理声称，关于对赋值右手端的变量的以前为真的任何命题在赋值之后仍然成立:

${\displaystyle {\frac {}{\{P[E/x]\}\ x:=E\ \{P\}}}\!}$ 

这里的${\displaystyle P[E/x]}$ 指示表达式P中所有的自由变量x都被替代为表达式E。

有效的三元组的兩個例子:

${\displaystyle \{x+1=43\land x=42\}\ y:=x+1\ \{y=43\land x=42\}\!}$ 

${\displaystyle \{x+1=N\}\ x:=x+1\ \{x=N\}}$ 

顺序规则

${\displaystyle {\frac {\{P\}\ S\ \{Q\}\ ,\ \{Q\}\ T\ \{R\}}{\{P\}\ S;T\ \{R\}}}\!}$ 

例如，考虑赋值公理的下列两个实例:

${\displaystyle \{x+1=43\}\ y:=x+1\ \{y=43\}}$ 

和

${\displaystyle \{y=43\}\ z:=y\ \{z=43\}}$ 

通过顺序规则，将得到:

${\displaystyle \{x+1=43\}\ y:=x+1;z:=y\ \{z=43\}}$ 

条件规则

${\displaystyle {\frac {\{B\wedge P\}\ S\ \{Q\}\ ,\ \{\neg B\wedge P\}\ T\ \{Q\}}{\{P\}\ {\textbf {if}}\ B\ {\textbf {then}}\ S\ {\textbf {else}}\ T\ {\textbf {endif}}\ \{Q\}}}\!}$ 

While规则

${\displaystyle {\frac {\{P\wedge B\}\ S\ \{P\}}{\{P\}\ {\textbf {while}}\ B\ {\textbf {do}}\ S\ {\textbf {done}}\ \{\neg B\wedge P\}}}\!}$ 

这里的P是循环不变条件。

推论规则

${\displaystyle {\frac {P^{\prime }\rightarrow \ P\ ,\ \lbrace P\rbrace \ S\ \lbrace Q\rbrace \ ,\ Q\rightarrow \ Q^{\prime }}{\lbrace P^{\prime }\ \rbrace \ S\ \lbrace Q^{\prime }\rbrace }}\!}$ 

全部正确性

上述规则只证明部分正确性。可以通过扩展版本的While规则证明全部正确性。

• 全部正确性的While规则:

${\displaystyle {\frac {\{P\wedge B\wedge t=z\}\ S\ \{P\wedge t<z\}\ ,\ P\rightarrow t\geq 0}{\{P\}\ {\textbf {while}}\ B\ {\textbf {do}}\ S\ {\textbf {done}}\ \{\neg B\wedge P\}}}\!}$ 

在本文中，除了维持循环不变条件，还能通过其值在每次重复期间递减的项就是这里的t的方式来证明终止。注意t必须从良定集合中取值，所以循环的每一步都通过递减有限链的成员来计数。

参见

• 契约式设计
• 动态逻辑
• 艾兹赫尔·戴克斯特拉
• 谓词变换者语义
• 程序验证

参考文献

引用

1. Hoare, C.A.R. (PDF). Communications of the ACM. October 1969, 12 (10): 576–585. doi:10.1145/363235.363259. （原始内容 (PDF)存档于2016-03-04）. 

来源

刊物文章

• C. A. R. Hoare. "An axiomatic basis for computer programming". Communications of the ACM, 12(10):576–585, October 1969. doi:10.1145/363235.363259

书籍

• Robert D. Tennent: "Specifying Software" (a recent textbook that includes an introduction to Hoare logic) ISBN 0-521-00401-2 [1] （页面存档备份，存于互联网档案馆）