(******************************************************************** A simple algorithm for computing the square root of a non-negative integer. See file [sqrt_why.v] for the proofs of obligations generated by Why. (c) Claude Marché 2002 **********************************************************************) let sqrt = fun (x : int) -> { x >= 0 } begin if x = 0 then 0 else if x <= 3 then 1 else let y = ref x in let z = ref (x+1)/2 in begin while !z < !y do { invariant z > 0 and y > 0 and z = (x/y+y)/2 and x < (y+1)*(y+1) and x < (z+1)*(z+1) variant y} y := !z; z := (x / !z + !z) / 2 done; !y end end { result * result <= x and x < (result+1)*(result+1) } (* Local Variables: mode: tuareg compile-command: "why sqrt.mlw" End: *)