functions

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

        sqrLoop : real * real -> real
        sqrLoop(r,x) == if accurate(r,x) then r else sqrLoop(approach(r,x), x);

        accurate : real * real -> bool  
        accurate(r,x) == abs(x - r*r) < 0.0001;

        approach : real * real -> real
        approach(r,x) == ((r + (x/r))/2);



        sqrt_esp (x : real) r : real
        pre x >= 0
        post r*r = x