(********************************************************************

  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: 
*)