Given: \[\begin{split} Q &: {\varnothing}= {{\mathbf{\top}}}\\ R &: res = n_0m_0\\ I &: (res + nm = n_0m_0) {\ \land \ }(n \geq 0)\\ B &: 0 < n\\ V &: n\\ S &: \{ res, n := res + m, n - 1 \} \end{split}\]
We are proving that: \(Q \to {wp\left(S_1, I\right)}\), where \(S_1\) is the statement before the loop. \[\begin{split} & S_1 &=& S_{11}; S_{12}\\ & S_{11} &=& res := 0\\ & S_{12} &=& {{if\left(n_0 \geq 0\right) \ \{ n, m := n_0, m_0 \}} \ {else \ \{ n, m := -n_0, -m_0 \}}}\\ & Q &\to& {wp\left(S_1, I\right)}\\ \iff & Q &\to& {wp\left(S_{11}; S_{12}, I\right)}\\ {\ ({\mathbf{§2}})} \iff & Q &\to& {wp\left(S_{11}, {wp\left(S_{12}, I\right)}\right)}\\ {\ ({\mathbf{§3}})} \iff & Q &\to& {wp\left(res := 0, (n_0 > 0 \to {wp\left(n, m := n_0, m_0, I\right)}) {\ \land \ }\\ (n_0 \leq 0 \to {wp\left(n, m := -n_0, -m_0, I\right)})\right)}\\ {\ ({\mathbf{§1}})} \iff & Q &\to& {wp\left(res := 0, (n_0 > 0 \to (res + n_0m_0 = n_0m_0) {\ \land \ }n_0 \geq 0) {\ \land \ }\\ (n_0 \leq 0 \to (res + n_0m_0 = n_0m_0) {\ \land \ }-n_0 \geq 0)\right)}\\ {\ ({\mathbf{§1}})} \iff & Q &\to& (n_0 > 0 \to (n_0m_0 = n_0m_0) {\ \land \ }n_0 \geq 0) {\ \land \ }\\ & & & (n_0 \leq 0 \to (n_0m_0 = n_0m_0) {\ \land \ }-n_0 \geq 0)\\ \iff & Q &\to& (n_0 > 0 \to n_0 \geq 0) {\ \land \ }(n_0 \leq 0 \to -n_0 \geq 0)\\ \iff & Q &\implies & {{\mathbf{\top}}}\end{split}\]