Proving Program {x=A, y=B} GCD(A,B) Correct

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

 

[berkeman]

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

 

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

 

[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

 

[Tony11235]

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

 

[Tony11235]

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

How do I perform induction on the loop cycles?

 

[NateTG]

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

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.

 

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