\[\begin{split} {wp\left(x :=e, R\right)} &= R[x \mapsto e] && {\ ({\mathbf{§1}})}\\ {wp\left(S1; S2, R\right)} &= {wp\left(S1, {wp\left(S2, R\right)}\right)} && {\ ({\mathbf{§2}})}\\ {wp\left({\text{assert }}B, R\right)} &= B {\ \land \ }R && {\ ({\mathbf{§3}})}\\ {wp\left({{if\left(B\right) \ \{ S1 \}} \ {else \ \{ S2 \}}}, R\right)} &= B \to {wp\left(S1, R\right)} {\ \land \ }\neg B \to {wp\left(S2, R\right)} && {\ ({\mathbf{§4}})}\\ {wp\left({if\left(B\right) \ \{ S1 \}}, R\right)} &= B \to {wp\left(S1, R\right)} {\ \land \ }\neg B \to R && {\ ({\mathbf{§5}})}\\ \end{split}\]
Variable names:
\[\begin{split} Q &: \text{Precondition}\\ R &: \text{Postcondition}\\ I &: \text{Loop invariant}\\ B &: \text{Loop branch condition}\\ V &: \text{Loop variant}\\ S &: \text{Statement inside loop}\\ \end{split}\]