Homework Help: Proving a program

1. Dec 14, 2005

Tony11235

{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. Dec 15, 2005

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

3. Dec 15, 2005

Tony11235

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.

4. Dec 15, 2005

NateTG

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

5. Dec 15, 2005

Tony11235

So basically show the loop invariant, gcd(x,y) = gcd(A,B), is always true?

6. Dec 15, 2005

Tony11235

How do I perform induction on the loop cycles?

7. Dec 15, 2005

NateTG

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.

8. Dec 15, 2005

Tony11235

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?