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

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

use int.Int
use int.ComputerDivision
use number.Gcd

val ref x: int
val ref y: int

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

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