# 霍尔逻辑

## 霍爾三元組

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

## 部分正确性

### 空语句公理

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

### 赋值公理模式

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

$\{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\} } \!$

### 推论规则

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

## 参考文献

### 书籍

• Robert D. Tennent: "Specifying Software" (a recent textbook that includes an introduction to Hoare logic) ISBN 0-521-00401-2 [1]