I have been trying to prove the following algorithm, without success.
Here is the C-Style pseudocode:
//j,k >= 0
int get_lcm(int j, int k){
int c = j;
int d = k;
while(c != d){
if(c < d){
c += j;
} else {
d += k;
}
}
return c;
}
I tried to find the loop invariant, which ended up being something like: $$ \begin{aligned} &c\le\text{LCM}(j,k) \wedge d\le\text{LCM}(j,k) \wedge c=aj \wedge d =bk\\ &(a,b \in N) \end{aligned} $$ I'm not sure how to proceed from here. I understand intuitively why the algorithm works, but I'm having trouble putting out an actual formal proof of it.
I need to come up with an invariant such that $c=d=LCM(j,k)$ when $c=d$. I'm having trouble showing how $c, d \le LCM(j,k)$ after one iteration.
Can anybody please help me? Thank you for your time.