{-

This program computes the gcd of two positive integers using the old
recipe of Euclides.

-}

prog gcdeuclid (x,y :: Int; g:: & Int)

pre x>0 /\ y>0

do

{ inv    x>0 /\ y>0 /\ (gcd x y = gcd x__0 y__0)
  metric x+y

  while x<>y do if x>y then x:=x-y else y:=y-x ;

  g := x
}

post g = gcd x__0 y__0 

lconst

gcd :: Int->Int->Int