isqrt.mlw 569 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10
module M

  use import int.Int
  use import ref.Ref

  function sqr (x:int) : int = x * x

  let isqrt (x:int) : int
    requires { x >= 0 }
    ensures { result >= 0 }
MARCHE Claude's avatar
MARCHE Claude committed
11
    ensures { sqr result <= x < sqr (result + 1) }
12 13 14 15 16 17 18 19 20 21 22 23 24 25 26
  = let count = ref 0 in
    let sum = ref 1 in
    while !sum <= x do
      invariant { !count >= 0 }
      invariant { x >= sqr !count }
      invariant { !sum = sqr (!count+1) }
      variant   { x - !count }
      count := !count + 1;
      sum := !sum + 2 * !count + 1
    done;
    !count

  let main () ensures { result = 4 } = isqrt 17

end