Proof of correctness of algorithm
To prove that the algorithm is correct, we assume that the loop invariant  $x_n + by_n = a$  is true per induction.

we have the following two cases:

case 1:

If MUL(a,b) returns true, then $x_n = 0$ and $y_n = n$,

so 

$x_n + by_n =a \rightarrow bn = a \rightarrow a$ is a multiplum of b

case 2:

if MUL(a,b) returns false, then $x_n \not= 0$, so we have

$x_n + by_n = a \rightarrow bn \not= a \rightarrow a$ is not a divisor of b.