Solution (source code)

= Solution

For integers $a,b$ not both zero, replace them first by their <absolute values>, then repeat <integer division>:

``
while b != 0:
    (a,b) := (b, a mod b)
return a
``

This is the <Euclidean algorithm>. Its <loop invariant> is that $\gcd(a,b)$ equals the original <greatest common divisor>. When $b>0$, the new remainder lies in $[0,b)$, so $b$ is a strictly decreasing nonnegative <loop variant>. At termination, $\gcd(a,0)=a$, proving correctness, including the case where one original input is zero.