 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.