WhyML

(* Greatest common divisor, using the Euclidean algorithm *)

module EuclideanAlgorithm

 use import mach.int.Int
 use import number.Gcd

 let rec euclid (u v: int) : int
 variant { v }
 requires { u >= 0 /\ v >= 0 }
 ensures { result = gcd u v }
 =
 if v = 0 then
   u
 else
   euclid v (u % v)

end

module EuclideanAlgorithmIterative

 use import mach.int.Int
 use import ref.Ref
 use import number.Gcd

 let euclid (u0 v0: int) : int
 requires { u0 >= 0 /\ v0 >= 0 }
 ensures { result = gcd u0 v0 }
 =
 let u = ref u0 in
 let v = ref v0 in
 while !v <> 0 do
   invariant { !u >= 0 /\ !v >= 0 }
   invariant { gcd !u !v = gcd u0 v0 }
   variant { !v }
   let tmp = !v in
   v := !u % !v;
   u := tmp
 done;
 !u

end