## Integer cubic root

Simple implementation in O(n^1/3).

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

**Topics:** Non-linear Arithmetic / Arithmetic

**Tools:** Why3

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

# Integer Cubic Root

Simple computation of the integer cubic root, using a loop and two auxiliary variables containing the square and the cube.

See also isqrt.mlw

module CubicRoot use int.Int use ref.Ref function cube (x: int) : int = x * x * x let cubic_root (x: int) : int requires { x >= 0 } ensures { cube (result - 1) <= x < cube result } = let ref a = 1 in let ref b = 1 in let ref y = 1 in while y <= x do invariant { cube (b - 1) <= x } invariant { y = cube b } invariant { a = b * b } variant { x - y } y <- y + 3 * a + 3 * b + 1; a <- a + 2 * b + 1; b <- b + 1 done; b end

download ZIP archive