Solution.
{m > 0 ∧ n > 0}
{m = m ∧ n = n ∧ m ≥ 0 ∧ n > 0}
x, y := m, n;
{x = m ∧ y = n ∧ x ≥ 0 ∧ y > 0}
{invariant : gcd(x, y) = gcd(m, n) ∧ x ≥ 0 ∧ y > 0}{rank function : x + y}
while x ≠ 0 ∧ y ≠ 0 do
{gcd(x, y) = gcd(m, n) ∧ x ≥ 0 ∧ y > 0 ∧ x ≠ 0 ∧ y ≠ 0}
{gcd(x, y) = gcd(m, n) ∧ x > 0 ∧ y > 0}
if x < y then
{gcd(x, y) = gcd(m, n) ∧ x > 0 ∧ y > 0 ∧ x < y}
1
x, y := y, x
{gcd(y, x) = gcd(m, n) ∧ y > 0 ∧ x > 0 ∧ y < x}
{gcd(x, y) = gcd(m, n) ∧ x > 0 ∧ y > 0 ∧ x ≥ y}
fi;
{gcd(x, y) = gcd(m, n) ∧ x > 0 ∧ y > 0 ∧ x ≥ y}
{gcd(x − y, y) = gcd(m, n) ∧ x − y ≥ 0 ∧ y > 0}
x := x − y
{gcd(x, y) = gcd(m, n) ∧ x ≥ 0 ∧ y > 0}
od
{gcd(x, y) = gcd(m, n) ∧ x ≥ 0 ∧ y > 0 ∧ ¬(x  0 ∧ y ≠ 0)}
{(x = 0 ∧ y = gcd(m, n)) ∨ (y = 0 ∧ x = gcd(m, n))}