Past exam of the year 1 of the computer science course of the University of Oxford / 2023 / Imperative programming / 1 / c

This is lower-bound search: return the first position whose value is at least the target, allowing the result to equal the array length. The notation for an empty suffix is vacuously true, so this also covers a target larger than every entry and the empty array. Assume a stable sorted array, ordered nondecreasingly.

def ternarySearch(a: Array[Int], x: Int): Int = {
  var lo = 0
  var hi = a.length
  while (lo < hi) {
    val third = (hi - lo) / 3
    val m1 = lo + third
    val m2 = hi - 1 - third
    if (a(m1) >= x) hi = m1
    else if (a(m2) < x) lo = m2 + 1
    else {
      lo = m1 + 1
      hi = m2
    }
  }
  lo
}

The loop invariant isInitially the excluded prefix and suffix are empty, so both quantified assertions hold. During an iteration, $lo\le m_1\le m_2<hi$. If $a(m_1)\ge x$, sortedness makes every later value at least $x$, so replacing hi by m1 preserves the right assertion. If the first test failed and $a(m_2)<x$, every earlier value is below $x$, so replacing lo by m2 + 1 preserves the left assertion. Otherwise $a(m_1)<x\le a(m_2)$; both new exclusions are valid, and lo = m1 + 1; hi = m2 retains exactly the unresolved middle. In that branch $m_1<m_2$, since a single value cannot satisfy both strict and nonstrict inequalities in opposite directions.

The nonnegative loop variant hi - lo strictly decreases. In fact, with old length $d$ and $q=\lfloor d/3\rfloor$, the three possible new lengths are $q,q,d-2q-2$, with the middle branch feasible only when nonnegative; each is at most $\lfloor d/3\rfloor$. At exit lo == hi, and the loop invariant is exactly the desired partition. The result is the unique lower-bound index, including the first equal entry when duplicates occur. This ternary lower-bound search uses $O(\log (N+1))$ comparisons and $O(1)$ auxiliary space, in the Big O notation word-operation model. The index formulas also avoid computing an overflowing 2 * length.