1. Limited time only! Sign up for a free 30min personal tutor trial with Chegg Tutors
    Dismiss Notice
Dismiss Notice
Join Physics Forums Today!
The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

Proof of Program Correctness

  1. Mar 5, 2015 #1
    1. The problem statement, all variables and given/known data

    Here is the program given:
    Code (Python):

    # 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.

    2. Relevant equations

    Iterative Method of Proving Program Correctness

    3. 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.
     
    Last edited by a moderator: Mar 5, 2015
  2. jcsd
  3. Mar 6, 2015 #2

    mfb

    User Avatar
    2016 Award

    Staff: Mentor

    You can find statements that are true independent of how often the two cases are hit. Hint: consider sums and differences.
     
  4. Mar 6, 2015 #3
    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.
     
  5. Mar 7, 2015 #4

    mfb

    User Avatar
    2016 Award

    Staff: Mentor

    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.
     
  6. Mar 7, 2015 #5
    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.
     
  7. Mar 7, 2015 #6

    mfb

    User Avatar
    2016 Award

    Staff: Mentor

    That is probably a matter of taste, I would multiply it with mn to get rid of fractions.
     
  8. Mar 7, 2015 #7
    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 ei = ai - bi 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.
     
  9. Mar 8, 2015 #8

    mfb

    User Avatar
    2016 Award

    Staff: Mentor

    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).
     
  10. Mar 8, 2015 #9
    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, thats 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 ?
     
  11. Mar 8, 2015 #10

    mfb

    User Avatar
    2016 Award

    Staff: Mentor

    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.
     
  12. Mar 9, 2015 #11
    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).
     
  13. Mar 9, 2015 #12

    mfb

    User Avatar
    2016 Award

    Staff: Mentor

    Even better if you don't need it. You can use it for k*m = l*n = b in some way I think.
     
Know someone interested in this topic? Share this thread via Reddit, Google+, Twitter, or Facebook

Have something to add?
Draft saved Draft deleted



Similar Discussions: Proof of Program Correctness
  1. It's correct or not (Replies: 2)

  2. Programming question (Replies: 6)

  3. Matlab Programming (Replies: 5)

Loading...