(* Euclidean division *)

use int.Int

val ref x : int
val ref y : int
val ref q : int
val ref r : int

let euclide ()
  requires { x >= 0 }
  ensures { x = q * y + r /\ 0 <= r < y }
  diverges (** we are not yet attempting to prove termination *)
  =
   q <- 0; r <- x;
   while r >= y do
      invariant { x = q * y + r /\ 0 <= r }
      r <- r - y; q <- q + 1
   done

let test ()
  diverges (** we are not yet attempting to prove termination *)
  =
  x <- 42; y <- 17; euclide(); (q,r)
  (* run test using "why3 execute imp_euclide.mlw Top.test" *)



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