Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Imperative programming resit / 1 / a

Use the remainder form of the Euclidean algorithm to compute the greatest common divisor, then divide both components of the fraction by it:The loop invariant is $a>0$, $b\ge 0$, and $\gcd (a,b)=\gcd (den,num)$. Initially it holds by symmetry of the greatest common divisor. For $b>0$, the integer division identity $a=qb+r$, with $0\le r<b$, shows that $a,b$ and $b,r$ have exactly the same common integer divisors. Thus the update preserves the loop invariant. The loop variant is the nonnegative integer $b$, which strictly decreases on each iteration. At exit $b=0$, so $a=\gcd (den,num)>0$. Dividing by $a$ preserves the rational number and makes the returned components coprime. In particular, zero is returned as $(0,1)$. No multiplication is needed, and all remainders remain within the original nonnegative Int range.