division.mlw 391 Bytes
Newer Older
1 2 3 4 5

(* Euclidean division *)

module Division

6 7
  use int.Int
  use ref.Refint
8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23

  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