(* Euclidean division *)

module Division

  use int.Int
  use ref.Refint

  let division (a b: int) : int
    requires { 0 <= a && 0 < b }
    ensures  { exists r: int. result * b + r = a && 0 <= r < b }
  =
    let q = ref 0 in
    let r = ref a in
    while !r >= b do
      invariant { !q * b + !r = a && 0 <= !r }
      variant   { !r }
      incr q;
      r -= b
    done;
    !q

end