## Euclidean division

**Authors:** Jean-Christophe Filliâtre

**Topics:** Arithmetic

**Tools:** Why3

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

(* 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

download ZIP archive