@function gcd : int, int -> int

@axiom A1: all x,y:int. x = y ==> gcd(x,y) = x  		 
@axiom A2: all x,y:int. x > y ==> gcd(x,y) = gcd(x-y,y) 	
@axiom A3: all x,y:int. x < y ==> gcd(x,y) = gcd(x,y-x)
		 
@requires x = m && y = n &&
          m > 0 && n > 0
@ensures x = gcd(m, n)

@program 
       @var x, y, m, n : int

	@invariant gcd(x,y) = gcd(m,n) && x >= 1 && y >= 1

     	while (not(x=y)) {
	      if (x > y) 
		   {x = x-y;}
	      else 
                   {y = y-x;}
     	}
@end
--