Proving the Correctness of Program g: How to Determine a Loop Invariant?

[NATURE.M]

Homework Statement

Here is the program given:

# PRE-condition: m and n are positive natural numbers.
# POST-condition: returns a tuple of natural numbers (k, l, b) such that k*m = l*n = b,
# and if natural number c is a positive multiple of both m and n then b <= c.
def g(m, n):
a=m
b=n
k=1
l=1

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

return (k, l, b)

The question asks to prove g is correct.

Homework Equations

Iterative Method of Proving Program Correctness

The Attempt at a Solution

Now I understand how to prove the correctness of an iterative program, but am confused on how to determine a proper Loop Invariant LI for this proof. I believe the if else condition in the while loop is confusing me, as I'm not sure if I should have two loop invariants or two cases for the LI.

Now consider the loop to iterate at least i times.
If I take the contents of the if statement ONLY I could easily write a = (1 + i)m and k = i + 1, as a rough start for the LI.
Likewise considering the contents of the else statement I have b = (1 + i)n and l = i + 1.

Now obviously this isn't true. But with the absence of the if/else statements I think I would know how to proceed. My issue is I don't know how many iterations occur where the if statement executes and how many occur where the else statement occurs. Also trying to relate it to the number of iterations of the loop, and post condition seems tricky. Any advice would be greatly appreciated.

 

[mfb]

You can find statements that are true independent of how often the two cases are hit. Hint: consider sums and differences.

 

[NATURE.M]

You can find statements that are true independent of how often the two cases are hit. Hint: consider sums and differences.

Okay so I'm able to see the relationship i = k + l - 2 where i is the number of iterations but I'm still having difficulty trying to relate a and b to i, m and n.

 

[mfb]

a=km, or k=a/m, and similar for l. You can plug that into the equation i=k+l-2 and simplify to get another equation.

 

[NATURE.M]

a=km, or k=a/m, and similar for l. You can plug that into the equation i=k+l-2 and simplify to get another equation.

Okay so if I just substitute we have i = a/m + b/n - 2. I'm not sure what you mean by simplify (or how this equation can be simplified). I'm sure that a and b should be written in terms of i but don't know how to do so. Otherwise the above statement is equivalent to i = k + l -2.

 

[mfb]

That is probably a matter of taste, I would multiply it with mn to get rid of fractions.

 

[NATURE.M]

Okay so here is what I have:

For i∈N, we define P(i): If there are at least i iterations, then i = k + l - 2 and mn(i+2) = na + mb.

Proof of LI:
Base Case: From the code when i=0 we see a=m, b=n, k=1, l=1. Then, k+l-2 = 1 + 1 -2 = 2-2 = 0 = i and mn(0+2) = 2mn = nm + mn = na + mb, as desired. So P(0) holds.
Inductive Step: Let i∈N. Assume P(i). Then, if there is an (i+1)th iteration of the loop then we have:
i + 1 = k + l - 2 + 1 = k + l - 1 (by IH) and mn(i+1+2) = mn(i + 3) = mni + 3mn = mni + 2mn + mn = mn(i+2) + mn = na + mb + mn (By IH). Now during the (i+1) iteration two cases can occur.
Case 0 : a<b Then a' = a + m (from the code). So na' + mb = n(a+m) + mb = na + mb + mn, as desired.
Case 1: a>=b Then b' = b + n (from the code). So na + mb' = na + m(b+n) = na + mb + mn, as desired.
Thus P(i+1) holds.

Now the next part is proving termination. Naturally one would think that e_i = a_i - b_i would work given the end condition is a = b. However, this will not work since the sequence formed will not be decreasing and will probably contain negative numbers.

Also I'm wondering if the second part of the post condition "if natural number c is a positive multiple of both m and n then b <= c" should also be incorporated into the Loop invariant.

 

[mfb]

If you just want to show that it terminates at some point: the difference (a-b) is limited and the loop making a new difference value out of the old one is an injective function operating in this limited range. That makes this difference (a-b) some repeating sequence, and you can also show that 0 is in the loop (which means your loop stops at some point).

 

[NATURE.M]

If you just want to show that it terminates at some point: the difference (a-b) is limited and the loop making a new difference value out of the old one is an injective function operating in this limited range. That makes this difference (a-b) some repeating sequence, and you can also show that 0 is in the loop (which means your loop stops at some point).

I feel like it would be better to use a decreasing sequence of natural numbers and use a corollary from well ordering principle that states any decreasing sequence of natural number is finite. At least, that's what I've typically seen looking through many proofs of correctness on iterative programs. The issue becomes finding an expression in terms of i that is decreasing. (a-b) is a sequence but not of the kind specified above.

Also I'm wondering about the second part of the post condition. Does my loop variant look thorough enough ? When I go to prove the post condition I assume termination of the loop (a=b end condition), so the first part of the post condition should be simple to show. But the second part worries me, and I don't see a direct relationship between the LI and "if natural number c is a positive multiple of both m and n then b <= c". Any thoughts ?

 

[mfb]

I don't see something that would always decrease, apart from the distance to the smallest common multiple - but you have to show that you reach it.

and I don't see a direct relationship between the LI and "if natural number c is a positive multiple of both m and n then b <= c". Any thoughts ?

That is basically the smallest common multiple that will lead to that condition.

 

[NATURE.M]

I don't see something that would always decrease, apart from the distance to the smallest common multiple - but you have to show that you reach it.

That is basically the smallest common multiple that will lead to that condition.

So what I take is that: for some t, s∈N, we have tm = sn = c. This would express any multiple of c. I'm wondering how to express the smallest common multiple.

And in the larger scheme of things, I feel the loop invariant condition isn't particularly helpful as I don't see any uses of it. Is this just me, or do you feel the same way? (we can totally prove first part of post condition from loop terminating condition, and the second part of the post condition doesn't really seem to relate to the LI).

 

[mfb]

Even better if you don't need it. You can use it for k*m = l*n = b in some way I think.