Prove correctness of iterative LCM algorithm

Question

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.

Answer 1

Assume j, k > 0.

You have your loop invariant. Every iteration, one of c or d gets larger. They cannot forever stay ≤ LCM (i, j), therefore the loop must finish.

Because c and d are multiples of i, j, they cannot change directly from being < LCM (i, j) to > LCM (i, j), instead there must be a step for each of c and d where it is equal.

If both are = LCM (i, j) then c = d and the algorithm exits. If one is = LCM (i, j) then the other one is smaller and gets increased.

Answer 2

I don't know how to write it down mathematically but may be I can do good with words to give you an idea.

You should ask yourself the question

What's the smallest possible LCM of j and k?

Ans- When the LCM is either j or k(When one divides the other without remainder).

So now what's happening in the loop

1. c is a multiple of j (since it is initialized with the value of j and increments by j whenever c is smaller than d).

2. Similarly d is a multiple of k.

Now let's come to the point

If j is the LCM then As long as j is greater than k , d will continue to increase unless d becomes equal to m*k where m is a factor of j.

If k is the LCM then As long as k is greater than j , c will continue to increase unless c becomes equal to n*j where n is a factor of k.

Mathematically, LCM can be defined as

LCM(j,k)=jn=km where n and m are the times j and k are added to themselves

So if an LCM exists then in the loop

c(the iterative multiple of j) must become j*n before becoming j*(n+1).

Similarly d(the iterative multiple of k) must become k*m before becoming k*(m+1). which is the same as saying that

c == d will be true at some point.