examples/cubic_root.mlw

   1
   2 (** {1 Integer Cubic Root}
   3
   4     Simple computation of the integer cubic root, using a loop and two
   5     auxiliary variables containing the square and the cube.
   6
   7     See also isqrt.mlw *)
   8
   9 module CubicRoot
  10
  11   use int.Int
  12   use ref.Ref
  13
  14   function cube (x: int) : int = x * x * x
  15
  16   let cubic_root (x: int) : int
  17     requires { x >= 0 }
  18     ensures  { cube (result - 1) <= x < cube result }
  19   =
  20     let ref a = 1 in
  21     let ref b = 1 in
  22     let ref y = 1 in
  23     while y <= x do
  24       invariant { cube (b - 1) <= x }
  25       invariant { y = cube b }
  26       invariant { a = b * b }
  27       variant   { x - y }
  28       y <- y + 3 * a + 3 * b + 1;
  29       a <- a + 2 * b + 1;
  30       b <- b + 1
  31     done;
  32     b
  33
  34 end