(** {1 MPRI lecture 2-36-1 "Proof of Programs"} *)

(* {2 GCD, Bezout coefficients} *)

use int.Int
use int.ComputerDivision

predicate _TO_BE_COMPLETED
constant _VARIANT_TO_BE_COMPLETED:int
constant _VALUE_TO_BE_COMPLETED:int
(* replace all occurrences of _TO_BE_COMPLETED below *)


let gcd (x:int) (y:int)
  requires { _TO_BE_COMPLETED }
  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 = _VALUE_TO_BE_COMPLETED in let ghost ref b = _VALUE_TO_BE_COMPLETED in
  let ghost ref c = _VALUE_TO_BE_COMPLETED in let ghost ref d = _VALUE_TO_BE_COMPLETED in
  while y > 0 do
    invariant { _TO_BE_COMPLETED  }
    variant { _VARIANT_TO_BE_COMPLETED }
    let r = mod x y in let ghost q = div x y in
    x <- y; y <- r;
    a <- _VALUE_TO_BE_COMPLETED; b <- _VALUE_TO_BE_COMPLETED;
    c <- _VALUE_TO_BE_COMPLETED; d <- _VALUE_TO_BE_COMPLETED;
  done;
  x

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