# 霍尔逻辑

## 霍爾三元組

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

## 部分正确性

### 空语句公理

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

### 赋值公理模式

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

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

### 推论规则

${\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规则:
${\displaystyle {\frac {\{P\wedge B\wedge t=z\}\ S\ \{P\wedge t

## 参考文献

### 引用

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

### 来源

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