1. Not finding help here? Sign up for a free 30min 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!

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?
Know someone interested in this topic? Share this thread via Reddit, Google+, Twitter, or Facebook

Have something to add?

Similar Discussions: Proving a program
  1. Verilog Program (Replies: 0)

  2. The program R (Replies: 2)

  3. MARIE Programming (Replies: 1)

  4. Programming question (Replies: 6)

  5. Matlab Programming (Replies: 5)