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!

Homework Help: Proving a program

  1. Dec 14, 2005 #1
    {x = A, y = B}
    while x != y do
    if x < y
    then y := y - x
    else x := x - y
    {x = gcd(A, B)}

    How do I prove that the program above is correct? A and B are whole numbers and gcd(A, B) stands for Greatest Commom Divisor. What's the best method for proving that it computes the gcd of A and B? It's not written in any specific language.
  2. jcsd
  3. Dec 15, 2005 #2


    User Avatar

    Staff: Mentor

    Can you show an example proof from your class? What techniques are you taught to use for a proof like this? What assumptions can you make about the compiler, etc.....?
  4. Dec 15, 2005 #3
    Methods that we have done include just various forms of induction. Can structural induction be used here? Mathematical induction? If so, I am not sure where to start when it comes to a program like this.
  5. Dec 15, 2005 #4


    User Avatar
    Science Advisor
    Homework Helper

    I would suggest induction on the loop cycles to show that:
    1. gcd(x,y) is always equal to gcd(A,B)
    2. x+y is strictly monotone decreasing
  6. Dec 15, 2005 #5
    So basically show the loop invariant, gcd(x,y) = gcd(A,B), is always true?
  7. Dec 15, 2005 #6
    How do I perform induction on the loop cycles?
  8. Dec 15, 2005 #7


    User Avatar
    Science Advisor
    Homework Helper

    Right, that will show that if you get a result, the result will be gcd(x,y).
    The other thing you need to show is that the program will terminate.
  9. Dec 15, 2005 #8
    I'm really only familiar with mathematical induction. I really do not see how to perform induction on the loops to show that the program is correct. Any examples?
Share this great discussion with others via Reddit, Google+, Twitter, or Facebook