Proving correctness of the Newton's Method for finding the square root of a number
I suggest you take some example values and see the pattern how Y actually changes. Observe that at the first iteration of the loop, Y may be too small, but only on the first iteration. Then you should see how Y changes after that. 

With that, you should find a much stronger loop invariant that lets you actually prove convergence (if TOL is small enough and we ignore arithmetic overflow).