(* GCD, Bezout coefficients *)

use int.Int
use int.ComputerDivision


let gcd (x:int) (y:int)
  requires { x >= 0 /\ y >= 0 }
  ensures  { exists a,b. result = a*x+b*y }
= let ref x = x in let ref y = y in
  label Init in
  let ghost ref a = 1 in let ghost ref b = 0 in
  let ghost ref c = 0 in let ghost ref d = 1 in
  while y > 0 do
    invariant { x >= 0 /\ y >= 0 }
    variant { y }
    invariant { x = a * x at Init + b * y at Init }
    invariant { y = c * x at Init + d * y at Init }
    let r = mod x y in let ghost q = div x y in
    x <- y; y <- r;
    let e = a in let f = b in
    a <- c; b <- d;
    c <- e - q * c; d <- f - q * d;
  done;
  x

(*
Local Variables:
compile-command: "why3 ide exo_bezout_sol.mlw"
End:
*)