Working out an invariant for a binary search

Question

I need hep working out what the invariant for this code would be. I think there can be multiple invariants but i don't really understand the topic and online resources i have found still dont really help. The code i made for the binary search is:

public class BinarySearchSqrt {

    /** Integer square root
     * Calculates the integer part of the square root
     * of n, i.e. integer s such that
     * s*s <= n and (s+1)*(s+1) > n
     * requires n >= 0
     */
    private static int iSqrt(int n) {
        int l = 0;
        int r = n;
        int m = ((l + r + 1) / 2);
        /* loop invariant
         * :
         * :
         */
        while (Math.abs(l - m) > 0) {
            m = ((l + r + 1) / 2);
            if ((m + 1) * (m + 1) > n) {
                r = m - 1;
            } else if ((m * m) < n) {
                l = m + 1;
            }
        }
        return m;
    }
    public static void main(String[] args) {
        System.out.println(iSqrt(15));
        System.out.println(iSqrt(16));
    }
}

This code uses binary search to find the square root of an integer, but if it is not a square number it should return the square root of the closest square number that is less than the integer.

The code works but i just dot really get what to put as the invariant is and how it shows what the correct value to return is. Any clues/explanation would be great, thank you.

Answer 1

OK, so this answer is almost half a year late, but here goes:

A loop invariant is simply something that holds before (and after) each iteration of a loop. So here, we need to find a condition that is valid each time the code is at the place marked with the arrow:

while (Math.abs(l - m) > 0) { //        <-------------
  m = ((l + r + 1) / 2);
  if ((m + 1) * (m + 1) > n) {
    r = m - 1;
  } else if ((m * m) < n) {
    l = m + 1;
  }
}

So here, at each iteration, you either have updated r so that the new r lies closer to the smallest integer <= sqrt(n), by reducing it, or you update l, so that the new l lies closer to the smallest integer <= sqrt(n), but by increasing it. So the loop invariant is simply:

l <= floor(sqrt(n)) <= r