isqrt.mlw 643 Bytes
Newer Older
1 2 3 4 5 6 7
module M

  use import int.Int
  use import ref.Ref

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

8 9 10
  lemma sqr_sum :
    forall x y : int. sqr(x+y) = sqr x + 2*x*y + sqr y

11 12 13
  let isqrt (x:int) : int
    requires { x >= 0 }
    ensures { result >= 0 }
MARCHE Claude's avatar
MARCHE Claude committed
14
    ensures { sqr result <= x < sqr (result + 1) }
15 16 17 18 19 20 21 22 23 24 25 26 27 28 29
  = 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