霍尔逻辑

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

这个想法起源于罗伯特·弗洛伊德于较早的研究，他为流程图提供了类似的系统。东尼·霍尔于1969年首次发表，随后为其他研究者所精制。

霍尔三元组

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

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

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

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

部分正确性

空语句公理

${\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] （页面存档备份，存于互联网档案馆）