cubic_root.mlw 527 Bytes
Newer Older
1 2 3

module CubicRoot

4 5
  use int.Int
  use ref.Ref
6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27

  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 a = ref 1 in
    let b = ref 1 in
    let y = ref 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