Codex @codex  0

Keep a running product of the fixed base. In particular, 1.0/n uses floating-point arithmetic, avoiding the truncation that integer division would introduce:

def eaLinear(n: Int): Double = {
  require(n > 0)
  val base = 1.0 + 1.0 / n.toDouble
  var k = 0
  var result = 1.0
  while (k < n) {
    result *= base
    k += 1
  }
  result
}

The loop invariant is

0 \leq k \leq n

and

res u lt = ba s e^{k}

. Initially the empty product is one. Multiplication by base and incrementing k preserve the invariant. The loop variant

n - k

decreases by one. On exit

k = n

, so the result is $e_{a} (n)$ , with exactly

n

multiplications and

O (n)

time complexity. With Double, the operational result is the rounded recurrence, rather than an exact real power; this distinction applies to the next two power computations too.

Past exam of the year 1 of the computer science course of the University of Oxford / 2018 / Imperative programming / 1 / b / Solution 2026-10-31

Generate each reciprocal factorial from the preceding one, instead of recomputing a factorial for every summand:

def eb(n: Int): Double = {
  require(n >= 0)
  var i = 0
  var term = 1.0
  var sum = 1.0
  while (i < n) {
    i += 1
    term /= i.toDouble
    sum += term
  }
  sum
}

The loop invariant is

0 \leq i \leq n

t er m = 1/ i!

, and

s u m = \sum_{j = 0}^{i} 1/ j!

. Initially

i = 0

and

0! = 1

. The division produces

1/ (i + 1)!

, which is then added to the previous partial sum. The loop variant is

n - i

. Consequently the returned value is $e_{b} (n)$ , using exactly

n

divisions and

n

additions, no multiplications, and

O (n)

time complexity. The slightly weaker precondition also permits the useful zero-term boundary case. For Double, small positive terms eventually cease to change sum because of floating-point rounding.

Past exam of the year 1 of the computer science course of the University of Oxford / 2018 / Imperative programming / 1 / c / Solution 2026-10-31

First rearrange the ratios so that the intermediate powers remain moderate:

e_{c} (n) = (n + 1) (1 + \frac{1}{n})^{n} - n (1 + \frac{1}{n - 1})^{n - 1} .

This avoids separately forming enormous powers such as

n^{n}

. Perform the two instances of exponentiation by squaring in one while loop, using coupled binary exponentiation:

def ec(n: Int): Double = {
  require(n > 1)
  val dn = n.toDouble
  var x = 1.0 + 1.0 / dn
  var y = 1.0 + 1.0 / (dn - 1.0)
  var k = n
  var l = n - 1
  var p = 1.0
  var q = 1.0
  while (k > 0 || l > 0) {
    if (k > 0) {
      if ((k & 1) != 0) p *= x
      k /= 2
      if (k > 0) x *= x
    }
    if (l > 0) {
      if ((l & 1) != 0) q *= y
      l /= 2
      if (l > 0) y *= y
    }
  }
  (dn + 1.0) * p - dn * q
}

With

A = 1 + 1/ n

and

B = 1 + 1/ (n - 1)

, the loop invariant is

k, l \geq 0

p x^{k} = A^{n}

, and

q y^{l} = B^{n - 1}

. Each active branch preserves its own power identity by the parity argument in part (a)(ii), and an inactive branch changes nothing. The loop variant is the mathematical integer

k + l

, which need not be computed in a fixed-width variable: it decreases whenever either exponent is positive. At exit

p = A^{n}

q = B^{n - 1}

, proving the returned expression is $e_{c} (n)$ . There are

O (lo g n)

iterations, at most four loop multiplications each, and two final multiplications. Converting n before adding one avoids integer overflow at Int.MaxValue.

The rearrangement avoids floating-point overflow in the original powers, but subtraction still combines two quantities of order

n

to obtain one of order one. Catastrophic cancellation can amplify their accumulated roundoff error. The mathematical

O (n^{- 2})

approximation error therefore does not imply that the Double implementation improves indefinitely as n grows.

Past exam of the year 1 of the computer science course of the University of Oxford / 2018 / Imperative programming / 2 / b / Solution 2026-10-31

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

0 \leq l o \leq hi \leq n, a [0.. l o) < x, x \leq a [hi .. n) .

Initially both excluded ranges are empty. If

a (mi d) < x

, sortedness justifies excluding every position through mid; otherwise it justifies excluding every position from mid onwards. The loop variant

hi - l o

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

l o = hi

, so lo satisfies the required partition, including when

n = 0

. Each new width is at most half the old width, rounded down; this gives

O (lo g (n + 1))

time complexity and constant space, conventionally

O (lo g n)

for nontrivial sizes.

Past exam of the year 1 of the computer science course of the University of Oxford / 2018 / Imperative programming / 2 / c / Solution 2026-10-31

A second binary search locates the first entry strictly greater than x:

def upperBound(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
}

def equalRange(a: Array[Int], x: Int): (Int, Int) =
  (lowerBound(a, x), upperBound(a, x))

For upper-bound search, the loop invariant is

0 \leq l o \leq hi \leq n

a [0.. l o) \leq x

, and

x < a [hi .. n)

; its loop variant is again

hi - l o

. The same midpoint and sortedness arguments prove preservation, termination and

O (lo g (n + 1))

time complexity. The first binary search in part (b) already has its own loop invariant and loop variant.

Let the two boundaries be

i, j

. There cannot be a value greater than

x

before the first value at least

x

, so

i \leq j

. Every entry between them is simultaneously at least and at most

x

, hence equals

x

. Entries before

i

are smaller and entries at or after

j

are larger, so the interval cannot be extended at either end. This proves the equal-range search result is maximal. If x is absent, i == j, both equal to its insertion position; this can be zero,

n

, or an interior gap. Two logarithmic searches still have logarithmic total time complexity. Computing an upper boundary as lowerBound(a, x+1) would introduce an unnecessary integer overflow bug at the largest integer.

Past exam of the year 1 of the computer science course of the University of Oxford / 2018 / Imperative programming / 3 / d / Solution 2026-10-31

Assume vector already satisfies the full representation invariant in part (b). Check the local bounds and value preconditions, then find the first index not smaller than the requested one:

def setElement(vector: Node, value: Double, index: Int): Unit = {
  require(vector != null)
  require(0 <= index && index < vector.index)
  require(value != 0.0 && !java.lang.Double.isNaN(value) &&
          !java.lang.Double.isInfinite(value))
  var p = vector.next
  while ((p ne vector) && p.index < index) p = p.next
  if ((p ne vector) && p.index == index) p.value = value
  else {
    val left = p.prev
    val fresh = new Node(value, index, left, p)
    left.next = fresh
    p.prev = fresh
  }
}

The search loop invariant says that the structure is unchanged and every ordinary linked list node passed has index smaller than index; p is the next candidate. The number of unpassed ordinary entries is a loop variant. The short-circuit evaluation prevents testing the header index as an ordinary entry. If an equal index exists, changing only its nonzero value preserves the representation invariant. Otherwise left and p delimit the unique insertion position: initializing both new links before redirecting their neighbors preserves reciprocal links and strict index order. Exactly the requested coordinate changes. With

k

stored entries, the search costs

O (k + 1)

and the splice costs constant time; checking the whole input structure is a caller obligation, rather than an unmentioned scan inside each call.

Past exam of the year 1 of the computer science course of the University of Oxford / 2018 / Imperative programming / 3 / e / Solution 2026-10-31

An already-zero entry needs no new linked list node:

def zeroElement(vector: Node, index: Int): Unit = {
  require(vector != null)
  require(0 <= index && index < vector.index)
  var p = vector.next
  while ((p ne vector) && p.index < index) p = p.next
  if ((p ne vector) && p.index == index) {
    val left = p.prev
    val right = p.next
    left.next = right
    right.prev = left
  }
}

The full input representation invariant is a precondition. The search has the same loop invariant and loop variant as in part (d). At exit, either p is the only stored entry with that index or none exists. In the first case, bypassing it in both directions removes exactly that coordinate and preserves the order of all remaining entries. This also works when its two neighbors are the same list header, leaving a self-linked empty structure. The header itself is never removed. The requested coordinate is zero and all others are unchanged, in

O (k + 1)

time complexity.

Past exam of the year 1 of the computer science course of the University of Oxford / 2018 / Imperative programming / 3 / f / Solution 2026-10-31

Append entries in increasing index order, keeping a tail reference so that repeated searches do not make construction quadratic:

def makeVector(elems: Array[Double]): Node = {
  require(elems != null)
  val h = makeZeroVector(elems.length)
  var tail = h
  var i = 0
  while (i < elems.length) {
    val v = elems(i)
    require(!java.lang.Double.isNaN(v) &&
            !java.lang.Double.isInfinite(v))
    if (v != 0.0) {
      val fresh = new Node(v, i, tail, h)
      tail.next = fresh
      h.prev = fresh
      tail = fresh
    }
    i += 1
  }
  h
}

The loop invariant is

0 \leq i \leq e l e m s . l e n g t h

, a valid circular representation of the nonzero entries in elems[0..i), a fixed header dimension elems.length, and tail eq h.prev. The next nonzero index is greater than every stored index; appending the fresh linked list node preserves reciprocal links, including tail.next eq h. The loop variant is elems.length-i. At exit the abstraction function yields exactly the input array as a vector. There is one pass and constant work per entry:

Θ (n)

time complexity for

n > 0

O (n + 1)

including emptiness, and

O (k + 1)

output storage for

k

nonzero entries. Both signs of floating-point zero are represented by absence.

Past exam of the year 1 of the computer science course of the University of Oxford / 2018 / Imperative programming / 3 / g / Solution 2026-10-31

Use the sorted sparse dot product merge, processing a coordinate only when it appears in both supports of a vector:

def dotProduct(vec1: Node, vec2: Node): Double = {
  require(vec1 != null && vec2 != null)
  require(vec1.index == vec2.index)
  var p = vec1.next
  var q = vec2.next
  var result = 0.0
  while ((p ne vec1) && (q ne vec2)) {
    if (p.index < q.index) p = p.next
    else if (q.index < p.index) q = q.next
    else {
      result += p.value * q.value
      p = p.next
      q = q.next
    }
  }
  result
}

Both structures must satisfy the representation invariant; equal dimension is checked explicitly. The loop invariant says that result contains exactly the products for all matching indices already passed, and that every skipped unequal index has zero in the other vector. The latter follows from sortedness: if p.index < q.index, that index cannot appear at q or later, and all earlier entries of the other vector have already been settled. Equality contributes its product exactly once. The total number of remaining ordinary entries is a loop variant; every iteration advances at least one cursor. Once either cursor reaches its header, all remaining entries pair with zeros. Thus the exact-arithmetic result is $\sum_{i} v ec 1_{i} v ec 2_{i}$ . With

k_{1}, k_{2}

stored entries, time complexity is

O (k_{1} + k_{2} + 1)

and auxiliary space is constant. Floating-point products and additions may round or overflow even when input coordinates are finite; no exact real-arithmetic accuracy claim is made for Double.

Past exam of the year 1 of the computer science course of the University of Oxford / 2018 / Imperative programming / 4 / d / i / Solution 2026-10-31

Place this object method inside the concrete class. Its precondition is the representation invariant; its postcondition is that the abstract data type state is unchanged and its left-to-right contents have been printed in bracket notation followed by a newline:

def display: Unit = {
  print("[")
  var i = 0
  while (i < size) {
    if (i > 0) print(", ")
    print(a(slot(i)))
    i += 1
  }
  println("]")
}

Assume ordinary sequential execution and successful output. The loop invariant is

0 \leq i \leq s i ze

, unchanged representation, and output consisting of [ followed by precisely the first

i

abstract values, separated by commas and spaces. The loop variant

s i ze - i

decreases. At exit the closing bracket completes the required display, including [] for emptiness. This takes

O (s i ze + 1)

output operations and constant space.

Past exam of the year 1 of the computer science course of the University of Oxford / 2018 / Imperative programming / 5 / d / iii / Solution 2026-10-31

Replace suspended recursive calls by an explicit stack for an inorder traversal. Save each original right child before overwriting that link:

def flattenIterative(): (Tree, Tree) = {
  val pending = new scala.collection.mutable.Stack[Tree]
  var current = root
  var start: Tree = null
  var end: Tree = null
  while (current != null || pending.nonEmpty) {
    while (current != null) {
      pending.push(current)
      current = current.left
    }
    val t = pending.pop()
    val nextSubtree = t.right
    t.left = end
    if (end == null) start = t else end.right = t
    t.right = null
    end = t
    current = nextSubtree
  }
  root = null
  (start, end)
}

The method belongs to the concrete class owning root. Clearing root records that ownership has transferred to the returned doubly linked list; callers retain both returned endpoints. The inner loop invariant says that the current subtree lies before all its pending ancestors in inorder traversal; pushing and descending left preserves this fact. Its loop variant is the number of entries along the remaining left-child path, a finite decreasing quantity.

The outer loop invariant says that start through end is precisely the already emitted sorted prefix, with reciprocal links and null outside endpoints. current and the pending ancestors describe exactly the remaining traversal in order; original links that are still needed have been retained. A pending ancestor has not yet had its right child overwritten. The next popped entry is therefore the next sorted entry. Saving nextSubtree preserves its future work before assigning t.right = null; linking it to end extends the prefix by exactly one entry. The number of original entries not yet emitted is an outer loop variant, since each full outer iteration emits one. At exit nothing remains, proving the same preservation and ordering postconditions as the recursive version.

Each entry is pushed and popped once, giving

O (n + 1)

time complexity and

O (h + 1)

auxiliary space. No new Tree entries are allocated. The historical mutable stack interface provides the push and pop operations used here; its later deprecation does not change their meaning.^[ref]

Past exam of the year 1 of the computer science course of the University of Oxford / 2018 / Imperative programming / 5 / d / ii / Solution 2026-10-31

Perform a destructive binary search tree flattening by converting both child subtrees and splicing their endpoints around the original root:

def flatten(t: Tree): (Tree, Tree) = {
  if (t == null) (null, null)
  else {
    val oldLeft = t.left
    val oldRight = t.right
    val (ls, le) = flatten(oldLeft)
    val (rs, re) = flatten(oldRight)
    t.left = le
    if (le != null) le.right = t
    t.right = rs
    if (rs != null) rs.left = t
    val start = if (ls == null) t else ls
    val end = if (re == null) t else re
    (start, end)
  }
}

Save the child references before changing their interpretation. The input is a finite binary search tree satisfying part (b), and no external client may simultaneously rely on the old tree links. By structural induction, the two recursive calls return disjoint, ordered doubly linked lists containing exactly their original entries. The binary search tree bounds place every left word before t.word and every right word after it. Splicing the left end, t, and the right start therefore preserves strict order and reciprocal links. A missing left list makes t.left null and t the start; a missing right list similarly makes t the end. The resulting outside links are null as required by part (i).

The recursive loop variant analogue is the strictly smaller number of entries in each child subtree. Every entry is processed once and incurs a constant number of link writes, so time complexity is

O (n + 1)

and recursion uses

O (h + 1)

auxiliary space. No new Tree entry is created; returning endpoint tuples and using a call stack are permitted auxiliary storage. The old binary search tree representation is consumed by this operation.

Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Imperative programming / 1 / a / Solution 2026-10-25

Accumulate the prefix by Horner's method in base two. digit-'0' converts either permitted digit to its numerical value:

var i = 0
var integerPart = 0.0
while (i < bin.length && bin(i) != '.') {
  integerPart = 2.0 * integerPart + (bin(i) - '0')
  i += 1
}

The loop invariant, in exact arithmetic, is that i is the number of processed digits before the point and

in t e g er P a r t = \sum_{j = 0}^{i - 1} (bin (j) -^{'} 0^{'}) 2^{i - 1 - j} .

Appending a digit shifts the old positional value by one binary place and adds that digit, which proves preservation. The loop variant is

bin . l e n g t h - i

. At exit, i is the binary-point index or the length if no point occurs, and integerPart is the value of the integer prefix. An empty prefix contributes zero. There is one multiplication per processed digit, with no separate powers or repeated divisions. Short-circuit evaluation prevents an out-of-range access when the point is absent.

For Double, this exact-arithmetic invariant describes the intended value; the operational value is the rounded Horner recurrence. Very long prefixes can lose precision or overflow, as discussed in part (g). A fixed-width return type cannot represent every finite binary digit string exactly.

Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Imperative programming / 1 / b / Solution 2026-10-25

Let point be the known point index. Work backwards so that each step uses just one division, rather than separately computing positional weights:

var j = bin.length - 1
var fractionalPart = 0.0
while (j > point) {
  fractionalPart = (fractionalPart + (bin(j) - '0')) / 2.0
  j -= 1
}

The loop invariant, under exact arithmetic, is

f r a c t i o na lP a r t = \sum_{t = j + 1}^{bin . l e n g t h - 1} (bin (t) -^{'} 0^{'}) 2^{j - t} .

Initially the suffix is empty. Incorporating digit

j

and dividing by two gives exactly the same formula with

j

replaced by

j - 1

. At exit

j = p o in t

, the result is $\sum_{t > p o in t} (bin (t) -^{'} 0^{'}) 2^{p o in t - t}$ . The loop variant is

j - p o in t

when a point exists. If a no-point input is handled by setting point=bin.length, the loop is skipped and the fractional contribution is zero;

max (0, j - p o in t)

is a loop variant covering that convention too. Trailing zeroes and an empty fractional suffix require no special arithmetic. Floating-point rounding qualifies the exact formula for long inputs.

Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Imperative programming / 1 / c / Solution 2026-10-25

Represent zero by one digit. Since int_part is nonnegative, a logical right shift is exactly integer division by two:

var digits = 1
var scratch = int_part
while (scratch >= 2) {
  scratch = scratch >>> 1
  digits += 1
}

The loop invariant is

d i g i t s \geq 1

and

scr a t c h = ⌊ in t_p a r t / 2^{d i g i t s - 1} ⌋

; for positive int_part, also

scr a t c h \geq 1

. The loop variant is scratch, strictly decreased whenever the guard holds. On exit, a positive input has

scr a t c h = 1

, yielding

2^{d i g i t s - 1} \leq in t_p a r t < 2^{d i g i t s}

. Therefore digits is the required width, including width one for zero. Shifting avoids an explicit multiplication or division in the code. This uses the supplied assumption that dec.toInt really is the mathematical floor; saturating or invalid conversions are not covered by that assumption.

Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Imperative programming / 1 / d / Solution 2026-10-25

Extract low bits and fill the integer positions from right to left:

var remaining = int_part
var pos = digits - 1
while (pos >= 0) {
  res(pos) = if ((remaining & 1) == 0) '0' else '1'
  remaining = remaining >>> 1
  pos -= 1
}

At the start of an iteration, the loop invariant says that positions

p os + 1, \dots, d i g i t s - 1

contain the correct low bits and

in t_p a r t = re mainin g 2^{d i g i t s - 1 - p os} + \sum_{t = p os + 1}^{d i g i t s - 1} (res (t) -^{'} 0^{'}) 2^{d i g i t s - 1 - t} .

The bitwise AND extracts the remainder modulo two; the shift supplies its quotient. These two facts preserve the loop invariant. The loop variant is

p os + 1

. The width established in part (c) ensures that remaining is zero at exit, so the first digits entries encode the whole integer part. For zero the single entry becomes '0'. There are no explicit multiplications or divisions, and no extra digit array is needed.

Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Imperative programming / 1 / e / Solution 2026-10-25

Generate the fractional bits by repeated doubling, keeping only the unconverted residual:

res(digits) = '.'
var fraction = dec - int_part.toDouble
var out = digits + 1
while (out < res.length) {
  fraction = 2.0 * fraction
  if (fraction >= 1.0) {
    res(out) = '1'
    fraction -= 1.0
  } else res(out) = '0'
  out += 1
}

Let

f_{0} = d ec - in t_p a r t

and

k = o u t - d i g i t s - 1

. The loop invariant is

0 \leq f r a c t i o n < 1

, the first

k

fractional digits have been written, and, in exact arithmetic,

f_{0} = \sum_{t = 1}^{k} (res (d i g i t s + t) -^{'} 0^{'}) 2^{- t} + f r a c t i o n 2^{- k} .

Doubling exposes the next digit, and subtracting that digit leaves the next residual in

[0, 1)

. This proves preservation. The loop variant is

res . l e n g t h - o u t

. The loop fills the whole suffix, even when the residual has become zero; subsequent bits are zero. There is one multiplication per output bit. With

F = res . l e n g t h - d i g i t s - 1

fractional positions, the result is truncated, with exact-arithmetic error $0 \leq d ec - v a l u e (res) < 2^{- F}$ . An integer has an all-zero suffix. No rounding-up step is performed.

Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Imperative programming / 2 / b / Solution 2026-10-25

Set aside the selected pivot at the end, array partitioning the other entries, then move the pivot to the separation index:

def partition(l: Int, r: Int): Int = {
  require(0 <= l && l < r && r <= a.length)
  def swap(i: Int, j: Int): Unit = {
    val t = a(i); a(i) = a(j); a(j) = t
  }
  val chosen = bestIndex(l, r)
  val x = a(chosen)
  swap(chosen, r - 1)
  var p = l
  var j = l
  while (j < r - 1) {
    if (a(j) < x) {
      swap(p, j)
      p += 1
    }
    j += 1
  }
  swap(p, r - 1)
  p
}

The loop invariant is

l \leq p \leq j \leq r - 1

a [l, p) < x

a [p, j) \geq x

, and

a (r - 1) = x

. The segment's multiset is unchanged and all entries outside it are unchanged. A low entry is swapped into the low segment; a high entry simply extends the high segment. The loop variant is

r - 1 - j

. At exit, exchanging the reserved pivot with a(p) gives $a [l, p) < x$ , $a (p) = x$ , and $a [p + 1, r) \geq x$ . The displaced value at the old pivot position was already at least

x

. Length one is handled by self-swaps and an empty loop. Duplicate pivot values belong to the high side. This costs

Θ (r - l)

time and

O (1)

auxiliary space.

Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Imperative programming / 2 / d / Solution 2026-10-25

Replace the tail call by updates to local bounds and a local rank:

def selectIterative(k: Int, l: Int, r: Int): Int = {
  require(0 <= l && l < r && r <= a.length)
  require(0 <= k && k < r - l)
  var low = l
  var high = r
  var rank = k
  while (high - low > 1) {
    val p = partition(low, high)
    val pivotRank = p - low
    if (rank == pivotRank) return a(p)
    if (rank < pivotRank) high = p
    else {
      rank -= pivotRank + 1
      low = p + 1
    }
  }
  a(low)
}

The loop invariant says that

l \leq l o w < hi g h \leq r

0 \leq r ank < hi g h - l o w

, and selecting rank rank in the active segment yields the originally requested order statistic. The original segment's multiset is preserved, and outside it no entries change. The updates are exactly the recursive reductions proved in part (c). The loop variant is

hi g h - l o w

; a non-returning iteration strictly decreases it. A one-entry segment has only rank zero, establishing the final return. Auxiliary space is $O (1)$ , rather than a potentially deep call stack.

Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Imperative programming / 3 / a / ii / Solution 2026-10-25

Use the already-filled prefix itself for membership tests. Long intermediates avoid overflow in the candidate calculations, while a checked conversion respects the required output type:

def recaman(a: Array[Int]): Unit = {
  if (a.length == 0) return
  a(0) = 0
  var i = 1
  while (i < a.length) {
    val candidate = a(i - 1).toLong - i.toLong
    var j = 0
    while (candidate > 0L && j < i && a(j).toLong != candidate) {
      j += 1
    }
    val next =
      if (candidate > 0L && j == i) candidate
      else a(i - 1).toLong + i.toLong
    require(next <= Int.MaxValue.toLong, "Sequence value exceeds Int")
    a(i) = next.toInt
    i += 1
  }
}

The outer loop invariant is

1 \leq i \leq a . l e n g t h

and

a (t) = r (t)

for

0 \leq t < i

. The inner loop invariant says that

0 \leq j \leq i

and no processed entry before j equals the positive candidate. Its guard either reaches the end of the prefix, finds the candidate, or immediately rejects a nonpositive candidate. Its loop variant is

i - j

. This establishes exactly the choice required by the recurrence, so the outer loop invariant is preserved. The outer loop variant is

a . l e n g t h - i

Extra storage is $O (1)$ beyond the supplied result array. Membership scans give an

O (N^{2})

upper bound for

N

output entries. Addition, unlike the subtraction branch, is not required to avoid repeats: at indices

20

and

24

the value

42

occurs twice. The code therefore does not try to enforce global distinctness. If an exact value eventually exceeds Int, the output interface cannot hold it; the check reports that limitation rather than wrapping the recurrence.