Wiki Agenda Contact Version française

Euclidean division


Authors: Jean-Christophe Filliâtre

Topics: Mathematics

Tools: Why3

see also the index (by topic, by tool, by reference, by year)


(* Euclidean division *)

module Division

  use import int.Int
  use import 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

download ZIP archive