What is the loop invariant for proving the LCM algorithm?

[flying2000]

algorithm to prove lcm:

a:=m
b:=n
while a != b
if a < b
a:= a + m
else
b:= b + n

//postcondition: a is the lcm(m,n)

what's the loop invariant?I thought it is(not sure):
lcm(ak, bk) = lcm(ak/m, bk/n) *lcm(m,n)
I am not sure and also impossible to prove my loop invariant...
Another loop invariant I thought is "ak=qm and bk=rn",but I don't know how to
show it's the lcm of m and n,
Thanks in advance!

 

[flying2000]

Forget it! problem soloved ...

Forget it! problem soloved ...

 

[Bartholomew]

I'm curious, how do you solve that?

 

[flying2000]

loop invariant..

I'm curious, how do you solve that?

the loop invariant should be
1)ak >=m and bk> =m
2)ak mod m=0 and bk mod n=0
3)ak<=lcm(m,n) and bk<=lcm(m,n)

U can prove a is the lcm(m,n) by these LI..

 

[Bartholomew]

Cool, I see.

 

[Bartholomew]

Wait, I think you also need ak > a(k-1) and bk > b(k-1)

That's not really a loop invariant though because it's not true until the second iteration.

I guess you could say something like "if k is > 1, then (that condition) is true."

 

[flying2000]

U right..

Wait, I think you also need ak > a(k-1) and bk > b(k-1)

That's not really a loop invariant though because it's not true until the second iteration.

I guess you could say something like "if k is > 1, then (that condition) is true."

I forget to mention that.. m,n>=1 is the precondition..

 

[Bartholomew]

No, that's not what I said. For example, what if the loop were:
for(i = 0; i < 10; i++)
{
a = m;
b = n;
}

That satisfies the loop invariants you gave, but it's not going to find the LCM.