霍尔逻辑

维基百科,自由的百科全书
跳转至: 导航搜索

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

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

霍爾三元組[编辑]

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

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

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

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

霍爾邏輯为简单的命令式编程语言的所有构造提供了公理推理规则。除了给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必须从良定集合中取值,所以循环的每一步都通过递减有限的成员来计数。

参见[编辑]

参考文献[编辑]

具体引用[编辑]

  1. ^ Hoare, C.A.R. An axiomatic basis for computer programming. Communications of the ACM. 1969-10, 12 (10): 576–585. 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]