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}
    begin
    while x != y do
    if x < y
    then y := y - x
    else x := x - y
    end
    {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

    berkeman

    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

    NateTG

    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)
    and
    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

    NateTG

    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