Showing that algorithm has STOP property and finding its computational complexity function
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.