module Division use int.Int use int.ComputerDivision use ref.Refint let division (a b: int) : (q: int, r: int) requires { 0 <= a && 0 < b } ensures { q * b + r = a && 0 <= r < b } = let ref r = a in let ref q = 0 in while r >= b do invariant { q * b + r = a && 0 <= r } variant { r } let ref c = b in let ref p = 1 in while c <= r do invariant { 0 < c <= 2*r } invariant { c > r -> exists c'. c = 2 * c' } invariant { c > r -> exists p'. p = 2 * p' } invariant { p * b = c } variant { r - c } c *= 2; p *= 2 done; c := div c 2; p := div p 2; r -= c; q += p done; (q, r) end