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

(** {2 Greatest Common Divisor: Euclid algorithm} *)

use int.Int
use int.ComputerDivision
use number.Gcd
(* mathematical definition of GCD already in the standard library *)

val ref x: int
val ref y: int

let gcd ()
  requires { x >= 0 /\ y >= 0 }
  diverges
  ensures  { result = gcd (old x) (old y) }
  = label L in
    while y > 0 do
      invariant { y >= 0 /\ x >= 0 }
      invariant { gcd x y = gcd (x at L) (y at L) }
      let r = mod x y in
      x <- y; y <- r
    done;
    x

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