# Rules of Hoare Logic

### Composition

$$
\frac{\{P\}\ \mathtt S\ \{Q\} \quad\quad \{Q\}\ \mathtt T\ \{R\}}
{\{P\}\ \mathtt S ; \mathtt T\ \{R\}}
$$

### Assignment

$$
\{P [\mathtt{exp}\,/\,\mathtt x] \}
\ \ \ \mathtt x:=\mathtt{exp} \ \ \
\{P \}
$$

### While

$$\frac{\{I \wedge \mathtt B \}\ \mathtt S\ \{I\}}{\{I \}\ \mathtt{while}\ B\ \mathtt{do}\ S\ \mathtt{done} \{\neg B \wedge I\}}$$

### If-Then-Else

$$
\frac{\{B \wedge P\}\ \mathtt S\ \{Q\} \quad\quad \{\neg B \wedge P \}\ \mathtt T\ \{Q\} }
{\{P\}\ \mathtt{if}\ B\ \mathtt{then}\ \mathtt S\ \mathtt{else}\ \mathtt T\ \mathtt{endif}\ \{Q\}
}$$

### Weakening

$${\frac{P'\Rightarrow P \quad\{P \}\ \mathtt S\ \{Q\} \quad Q\Rightarrow Q'}{\{P' \}\ \mathtt S \ \{Q'\}}}$$