Compute the square root of a positive integer using binary search

Question

The requirement is to find the square root of a positive integer using binary search and the math property that square root of a number n is between 0 and n/2, and the required answer is "floored", meaning mySqrt(8) is to return 2.

Please comment on the efficiency, and if possible, the loop invariants in terms of correctness:

class Solution(object):
    def mySqrt(self, x):
        """
        :type x: int
        :rtype: int

        Loop invariant: 

            The answer is always in the range [low, high] inclusive,
            except possibly:

                1) low == high == mid, and mid * mid == x and 
                   any of low, high, or mid can be returned as the answer.

                2) if there is no exact answer and the floor is to be 
                   returned, then low > high by 1. Since sq != x,
                   so either low or high is set inside the loop.

                   If low gets set and gets pushed up, it is pushed up too much. 
                   So when low > high by 1, low - 1 is the answer and it is the same 
                   as high, because low > high by 1.

                   If high gets set and gets pushed down, high can be
                   the correct answer. When low > high, it is by 1,
                   and high is the correct floor value to be returned. 
                   (since there is no perfect square root and the floor is required)

            0 <= low <= answer <= high <= n//2 + 1

                where answer is floor(sqrt(x)) to be found,
                except if low > high and the loop will exit.

            Each loop iteration always makes the range smaller.

        If the range is empty at the end, low is > high by 1, and high is 
            the correct floored value, and low is the ceiling value, so high is returned.
        """

        low = 0;
        high = x//2 + 1;

        while (low <= high):
            mid = low + (high - low) // 2;
            sq = mid * mid;
            if (sq == x):
                return mid;
            elif (sq > x):
                high = mid - 1;  # sq exceeds target, so mid cannot be the answer floored, but when high is set to mid - 1, then it can be the answer
            else:
                low = mid + 1;   # (here sq < x, and mid might be the answer floored, so when low is set to mid + 1, then low might be too big, while high is correct)

        return high;

Answer 1

• Your comments on the elif / else part are too long to be just after the statements

• Don't use semicolons (;) in Python.

• This is a refactored version of the code

import math

class Solution(object):
    def mySqrt(self, x):
        """
        :type x: int
        :rtype: int

        Returns floor(sqrt(x))
        """
        low = 0
        high = x//2 + 1

        """
        It is proved that 0 <= sqrt(x) <= x/2, so
        we run a dichotomic in [0, x/2] to find floor(sqrt(x))

        Loop analysis:
        * Initialization: low = 0 and high = x/2 + 1 
        * Termination: |high-low| is reduced each iteration,
          as shown in lines high = mid - 1 and low = mid + 1.
        * Invariant: low <= floor(sqrt(x)) <= high.
          Let mid be (low + high)/2.
            - If mid^2 <= x < (mid+1)^2,
              then mid is floor(sqrt(x)) and just return it.
            - If mid^2 > x, search for values smaller than mid.
            - Otherwise, if mid^2 < x, search within higher values.
        """
        while (low <= high):
            mid = (low + high) // 2
            sq = mid * mid
            sq_next = (mid+1)*(mid+1)
            if (sq <= x < sq_next):
                return mid
            elif (sq > x):
                high = mid - 1
            else:
                low = mid + 1

for i in range(1, 26):
  assert(math.floor(math.sqrt(i)) == Solution().mySqrt(i))