Integer Square Root Algorithm I'm currently working my way through David M. Bressoud's "Factorization and Primality Testing", and I'm struggling with an exercise (exercise 5.7) that asks the reader to prove that the following algorithm produces the greatest integer less than or equal to the square root of $n$:
\begin{align} 
\text{INITALIZE:} \quad &\text{READ} \;n \\ 
&a \leftarrow n \\ 
&b \leftarrow \lfloor (n+1)/2 \rfloor \\\\
\text{MYSTERY_LOOP:} \quad &\text{WHILE} \: b < a \; \text{DO} \\ 
&\quad a \leftarrow b \\
&\quad b \leftarrow \lfloor (a \times a + n) / (2 \times a) \rfloor \\\\
\text{TERMINATE:}\quad &\text{WRITE} \; a
\end{align} 
I know from real analysis that the sequence $x_{m+1} = \frac{x_m^2 + n}{2 x_m}$ converges to the square root of $n$ (for any sensible $x_0$), so morally, I can believe that the above algorithm converges to the integer square root of $n$.
How do we formally prove that the above algorithm works (i.e. terminates in a finite number of steps, such that $a^2 \leq n$ and $(a+1)^2 >n$), and moreover, why start the iterations with $b = \lfloor\frac{n+1}{2} \rfloor$? Is $\lfloor\frac{n+1}{2} \rfloor$ just a very crude approximation? What is its significance? 
I have tried splitting the floor into a real part minus a part between 0 and 1 (i.e. $\lfloor x \rfloor = x - \{x\}$), but I haven't been able to get very far with this. 
In addition, do we have the same quadratic convergence that we get when we compute the (ordinary) square root using Newton's method?

Using the notation of the $a$ and $b$ is only necessary when programming.
You have correctly identified that the algorithm gives a sequence of values, which I will call (as you did) the $x_m$.
We thus have the relationship $x_{m+1} = \lfloor \frac{x_m^2 + n}{2 x_m} \rfloor$
Starting with $x_0=n$ gives $x_{1} = \lfloor \frac{x_0^2 + n}{2 x_0} \rfloor=\lfloor \frac{n^2 + n}{2 n} \rfloor = \lfloor \frac{n+1}{2} \rfloor$, which answers one of your questions. It also demonstrates that the change from $x_0$ to $x_1$ is always a decrease (unless n=1).
Given two successive terms of the sequence $x_m$ and $x_{m+1}$, there are three possible outcomes:
1) $x_{m+1}=x_m$
2) $x_{m+1}<x_m$
3) $x_{m+1}>x_m$
Let's consider these in turn.
1) $x_{m+1}=x_m$
$\lfloor \frac{x_m^2 + n}{2 x_m} \rfloor=x_m$
The $floor$ function can be dealt with by expressing $\lfloor \frac{x_m^2 + n}{2 x_m} \rfloor=\frac{x_m^2 + n}{2 x_m}-p$ where $0 \le p < 1$
Thus we have $\frac{x_m^2 + n}{2 x_m}-p=x_m$
Rearranging gives $\frac{n-x_m^2}{2 x_m}=p$
Since $0 \le p < 1$, we can say that $0 \le \frac{n-x_m^2}{2 x_m} < 1$
Considering this in two parts, we have first:
$0 \le \frac{n-x_m^2}{2 x_m}$
$x_m$ is positive, so $0 \le {n-x_m^2}$
$x_m^2 \le n$
$x_m \le \sqrt n$
Then:
$\frac{n-x_m^2}{2 x_m} < 1$
${n-x_m^2} < {2 x_m}$
$n<x_m^2 + 2 x_m$
Completing the square,
$n+1<x_m^2 + 2 x_m+1$
$n+1<(x_m + 1)^2$
$\sqrt {n+1}<x_m + 1>$
$\sqrt {n+1}-1<x_m $
Putting the two inequalities back together gives us $\sqrt {n+1}-1<x_m \le \sqrt n$
It can be shown (binomial expansion) that $\sqrt {n+1}-1>\sqrt n -1 $ so we have:
$\sqrt n - 1 <x_m \le \sqrt n$
So if the sequence converges to a value, then this will be the largest integer less than or equal to the square root of $n$.
It could be, however, that the values oscillate without converging. What about those situations?
Moving on:
2) $x_{m+1}<x_m$
Following the same method as before, we have
$\frac{x_m^2 + n}{2 x_m}-p<x_m$
$\frac{n - x_m^2}{2 x_m}<p$
$\frac{n - x_m^2}{2 x_m}<1$
${n - x_m^2}<{2 x_m}$
$n<x_m^2+2 x_m$
$n+1<x_m^2+2 x_m+1$
$n+1<(x_m+1)^2$
$\sqrt {n+1}<x_m+1$
$x_m>\sqrt {n+1}-1$
As before, this gives $x_m>\lfloor \sqrt n \rfloor$
If there are two successive decreases in value, then both $x_m$ and $x_m+1$ will be greater than $x_m>\lfloor \sqrt n \rfloor$, but the values will be moving closer to $x_m>\lfloor \sqrt n \rfloor$, thus having convergence.
3) $x_{m+1}>x_m$
$\frac{x_m^2 + n}{2 x_m}-p>x_m$
$\frac{n - x_m^2}{2 x_m}>p$
We know that $p \ge 0$, so $\frac{n - x_m^2}{2 x_m} \ge 0$
$n - x_m^2 \ge 0$
$x_m^2 \le n$
$x_m \le \sqrt n$
This means that an increase in the values of the sequence only happens if the value in the sequence is less than or equal to the square root. There cannot be an infinite run of increases because eventually the value will become greater than the square root. Therefore there must eventually be a decrease in the values of the sequence.
