霍尔逻辑

Hoare 逻辑(也叫做Floyd–Hoare 逻辑)是英国计算机科学家東尼·霍爾开发的形式系统，随后为 Hoare 和其他研究者所精制。它发表于東尼·霍爾 1969年的论文"计算机程序的公理基础"中。这个系统的用途是为了使用严格的数理逻辑推理计算机程序的正确性提供一组逻辑规则。

Hoare 认可罗伯特·弗洛伊德的早期贡献，他为流程图提供了类似的系统。

Hoare 逻辑的中心特征是Hoare 三元组。这种三元组描述一段代码的执行如何改变计算的状态。Hoare 三元组有如下形式

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

这里的 P 和 Q 是断言而 C 是命令。P 叫做前条件而 Q 叫做后条件。断言是谓词逻辑的公式。这个三元组在直觉上读做: 只要 P 在 C 执行前的状态下成立，则在执行之后 Q 也成立。注意如果 C 不终止，也就没有"之后"了，所以 Q 在根本上可以是任何语句。实际上，你可以选择 Q 为假来表达 C 不终止。

这叫做"部分正确(partial correctness)"的。如果 C 终止并且在终止时 Q 是真，则表达式就是"全部正确(total correctness)"的。终止必须被单独证明。

Hoare 逻辑为简单的命令式编程语言的所有构造提供了公理和推理规则。除了给 Hoare 论文中的简单语言的规则，其他语言构造的规则也已经被 Hoare 和很多其他研究者开发出来了。包括并发、过程、goto语句，和指针。

部分正确性 [编辑]

空语句公理 [编辑]

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

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

赋值公理模式 [编辑]

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

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

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

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

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

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

顺序规则 [编辑]

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

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

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

和

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

通过顺序规则，将得到:

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

条件规则 [编辑]

$\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 规则 [编辑]

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

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

推论规则 [编辑]

$\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 规则:

$\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 必须从良定集合中取值，所以循环的每一步都通过递减有限链的成员来计数。

参见 [编辑]

引用 [编辑]

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]