The Hoare assignment axiom

\[\vdash \{P[E/V]\} V:=E \{P\} \]

The Floyd assignment axiom

\[\vdash \{P\} V:=E \{\exist v.\ (V=E[v/V]) \wedge P[v/V]\} \]

Precondition strengthening

\[\frac{\vdash P \Rightarrow P',\vdash\{P'\}C\{Q\}}{\vdash\{P\}C\{Q\}} \]

Postcondition weakening

\[\frac{\vdash\{P\}C\{Q'\},\vdash Q' \Rightarrow Q}{\vdash\{P\}C\{Q\}} \]

Specification conjunction

\[\frac{\vdash\{P_1\}C\{Q_1\},\vdash\{P_2\}C\{Q_2\}}{\vdash\{P_1 \wedge P_2\}C\{Q_1 \wedge Q_2\}} \]

Specification disjunction

\[\frac{\vdash\{P_1\}C\{Q_1\},\vdash\{P_2\}C\{Q_2\}}{\vdash\{P_1 \vee P_2\}C\{Q_1 \vee Q_2\}} \]

The sequencing rule

\[\frac{\vdash\{P\}C_1\{Q\},\vdash\{Q\}C_2\{R\}}{\vdash\{P\}C_1;C_2\{R\}} \]

The derived sequencing rule

\[\frac{\vdash\{P_1\}C_1\{Q_1\},\vdash\{P_2\}C_2\{Q_2\},...,\vdash\{P_n\}C_n\{Q_n\},\vdash P \Rightarrow P_1,\vdash Q_1 \Rightarrow P_2,\vdash Q_2 \Rightarrow P_3,...,\vdash Q_n \Rightarrow Q}{\vdash\{P\}C_1;...;C_n\{Q\}} \]

The conditional rule

\[\frac{\vdash\{P \wedge S\}C_1\{Q\},\vdash\{P \wedge \neg S\}C_2\{Q\}}{\vdash\{P\}\ \mathsf{IF}\ S\ \mathsf{THEN}\ C_1\ \mathsf{ELSE}\ C_2 \{Q\}} \]