Showing that algorithm has STOP property and finding its computational complexity function The task is to show that given algorithm has STOP property and to find its computational complexity function.

$\alpha:$ $n \ge 0$

void fun(int n) { 
    a=0;b=n+1; 
    while ((a + 1) != b) {
        p = (a + b)/2;
        if (p ∗ p &gt; n) 
            b = p; 
        else a = p; 
    }
}


I have already proven its partial correctness as it was also part of the task, however I do have problem with these things that I have mentioned above.

I think it can be easily seen that it is gonna stop as 'a' is getting bigger and bigger, but I don't really know how to notate or show it in more mathematical way. 

Thanks for your help.
You have already proven $a &lt; b$. Let $g$ be the gap between $a$ and $b$, so $b - a$.


Show that the algorithm terminates when $g = 1$.
Show that when $g &gt; 1$ we have as postcondition that the new $g' \leq \lceil g/2 \rceil$ in the loop body, and thus $g' &lt; g$.
Show that it's impossible to skip $g = 1$, and thus the algorithm must terminate.