Let a be the given enclosing array. A two-way array partition needs only one scan, and does not require the pivot to occur in the array:
def partition(l: Int, r: Int, p: Int): Int = {
  require(0 <= l && l <= r && r <= a.length)
  var k = l
  var j = l
  while (j < r) {
    if (a(j) < p) {
      val t = a(k)
      a(k) = a(j)
      a(j) = t
      k += 1
    }
    j += 1
  }
  k
}
The loop invariant is , every entry of is less than , every entry of is at least , and the segment's multiset is unchanged. Entries outside are unchanged. When a(j)<p, swapping it into position k extends the low part; if k<j, the displaced entry was in the high part and remains there after j advances. If k==j, the self-swap is harmless. The other branch simply extends the high part. The loop variant is . At exit , so the returned has the required separation property, including empty segments and arbitrarily many duplicate entries. The time complexity is and auxiliary space complexity is .
Keep a deficient interval of possible values and only the array segment containing occurrences from that interval. This is missing-value search by deficient value intervals:
def missing(): Int = {
  val n = a.length
  var lo = 0L
  var hi = n.toLong + 1L
  var l = 0
  var r = n
  while (hi - lo > 1L) {
    val p = lo + (hi - lo) / 2L
    val k = partition(l, r, p.toInt)
    if ((k - l).toLong < p - lo) {
      hi = p
      r = k
    } else {
      lo = p
      l = k
    }
  }
  lo.toInt
}
The precondition is that every original entry lies in . The loop invariant is
together with: every active entry lies in , and every original occurrence with a value in that interval is in the active segment. The whole array remains a permutation of its initial contents. Initially these assertions follow from the precondition and .
After array partitioning, the low subinterval has occurrences and possible values. If it is deficient, retaining it preserves the loop invariant. Otherwise , while the original active count is strictly less than ; subtraction gives
Thus the high subinterval is deficient and retaining it also preserves the loop invariant. Discarded occurrences lie outside the new candidate interval. The loop variant is the positive integer , which strictly decreases because the midpoint is strictly internal. At exit the interval has one possible value and fewer than one occurrence, so lo is absent from the entire original array. For the loop is skipped and zero is returned. The Long value bounds avoid overflowing ; every internal pivot is at most , so its checked mathematical range fits Int.
For the time complexity, let be the interval width and its active occurrence count before iteration . The loop invariant gives , and binary search gives . Each two-way array partition costs . Until the width reaches one, the widths are bounded by , so the total scan work is bounded by a geometric series plus loop overhead: overall, hence for positive . Partitioning the full array again at every iteration would instead lose this bound. Auxiliary space complexity is .