-- Square Root (LSB, 2006)


-- specification

functions

sq (x:real, e:real)t:real
post abs(x-t*t) < e;



-- functional implementation

functions

sqrt : real * real -> real
sqrt(x,e) == sqrLoop(1,x,e)
pre (x > 0);

sqrLoop : real * real * real -> real
sqrLoop(g,x,e) == if (abs(x-(g*g)) < e) 
                  then g
		  else sqrLoop((g+x/g)/2,x,e);



-- imperative implementation


operations

SquareRoot : real * real ==> real
SquareRoot (r,e) ==
  (dcl x:real := 1,
       nextx:real := r;
   while abs (x - nextx) >= e * x do
     ( x := nextx;
       nextx := ((r / x) + x) / 2;
     );
   return nextx
  )
pre (r > 0);


TSquareRoot : real * real ==> real
TSquareRoot (r,e) == if (r<0) then return -SquareRoot(abs(r),e)
                              else return SquareRoot(r,e);