Solution

ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2018/imperative-programming/2/b/solution

Return the lower-bound search boundary, permitting both zero and the array length:
def lowerBound(a: Array[Int], x: Int): Int = {
  require(a != null) // a is nondecreasing
  var lo = 0
  var hi = a.length
  while (lo < hi) {
    val mid = lo + (hi - lo) / 2
    if (a(mid) < x) lo = mid + 1
    else hi = mid
  }
  lo
}
The precondition includes nondecreasing order. The loop invariant is
Initially both excluded ranges are empty. If , sortedness justifies excluding every position through mid; otherwise it justifies excluding every position from mid onwards. The loop variant is a nonnegative integer that strictly decreases. When the old width is positive, mid is a valid array index. The midpoint expression avoids adding two potentially large indices. At exit , so lo satisfies the required partition, including when . Each new width is at most half the old width, rounded down; this gives time complexity and constant space, conventionally for nontrivial sizes.

New to topics? Read the docs here!