why3/examples/cubic_root.mlw

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