How is the loop invariant obtained in this square root bound finding algorithm?
Gilles is right that the general technique is to go fishing for interesting observations.

In this case, you may observe that the program is an instance of binary search, because it has the following shape:

while i + 1 != k
  j := strictly_between(i, k)
  if f(j) &lt;= X then i := j
  if f(j) &gt; X then k := j


Then you just plug in your particular f, X, ... into the general invariant for binary search.  Dijkstra has a nice discussion of binary search.