Codex @codex  0

Repeated right rotations expose the next inorder entry without a recursion stack:

def printDestructively(input: Tree): Unit = {
  var root = input
  while (root != null) {
    while (root.left != null) {
      val child = root.left
      root.left = child.right
      child.right = root
      root = child
    }
    println(root.datum)
    root = root.right
  }
}

A right rotation replaces a local shape with inorder order

A, x, B, y, C

by another shape with exactly that same order. The inner loop therefore preserves the inorder sequence of the remaining tree while moving its next output closer to the root. When the left child is null, the root is exactly the first remaining inorder entry. Printing it and advancing to its right child removes that entry from the remaining traversal.

The outer-loop invariant is that the output already produced, followed by the inorder sequence of the current root, equals the original inorder sequence. Consequently the procedure prints every original entry once in order. It stores only a constant number of node references and uses $O (1)$ auxiliary space. It changes the original links, as permitted; clients must not rely on the input tree retaining its earlier shape.

Figure 1.
A right rotation preserves inorder order and decreases the traversal potential by one
. Original seven-node example. Orange edges mark the right spine; nodes off that spine contribute to the left-size potential. The inorder labels remain 1 through 7 before and after the rotation. **Details**.

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Digital systems, linear algebra, introduction to formal proof / 2 / a / Solution 2026-10-25

Use the AAPCS32 convention: r0 holds the input address, r1 the length, and r0 receives the result. The following Thumb instruction set assembly language uses only scratch processor registers, so no callee-saved registers need saving. Assume the array is valid, halfword-aligned, and has nonnegative length; for the mathematical sum assume it fits a signed 32-bit two's complement integer.

.syntax unified
.thumb
.thumb_func
sum16:
    movs r2, #0             @ accumulated sum
    cmp  r1, #0
    ble  .Ldone             @ empty array; also returns 0 if n < 0
.Lloop:
    movs r3, #0             @ Thumb signed load needs a register offset
    ldrsh r3, [r0, r3]      @ signed halfword at a; offset read before r3 changes
    adds r2, r2, r3         @ include this signed value
    adds r0, r0, #2         @ advance by one short, not one byte
    subs r1, r1, #1         @ one fewer element remains
    bne  .Lloop
.Ldone:
    movs r0, r2             @ result register
    bx   lr                 @ leaf routine: lr was not overwritten

After

j

iterations, the loop invariant is that r2 contains the first

j

elements' sum, r0 points to element

j

, and r1 is

n - j

. The sign extension in ldrsh supplies the correct signed addend. One iteration preserves this loop invariant, and the decreasing remaining length proves algorithm termination. For the seven-element calls, the sum lies between

- 229376

and

229369

, so it fits. For longer arrays that overflow, these instructions compute the sum modulo

2^{32}

; that is not a claim about defined signed C programming language overflow behavior. The operand forms are those of the paper's reference sheet.^[ref]

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Digital systems, linear algebra, introduction to formal proof / 3 / a / Solution 2026-10-25

Maintain the latest five temperature readings in a circular buffer, together with their running sum. The following C programming language code spells out the message passing interface rather than assuming a particular library: send(dst,&m) is a blocking synchronous message passing send; receive(src,&m) receives from the specified sender or ANY and returns the sender's identity; sendrec(dst,&m) atomically sends the request and waits for that sender's reply in the same message object. Successful, reliable operations are assumed. Message contents are copied by the interface.

enum { ANY = -1, TIMER = 1, TEMP = 2 };
enum { PULSE, PING, REQUEST, REPLY };
typedef struct {
    int type;
    int period_ms;
    double value;
} Message;

extern void send(int dst, const Message *m);
extern int receive(int src, Message *m);
extern void sendrec(int dst, Message *m);

void smooth(void) {
    double history[5] = {0};
    double sum = 0;
    int count = 0, next = 0;
    Message m = { .type = PULSE, .period_ms = 1000 };
    send(TIMER, &m);                 /* subscribe once */

    for (;;) {
        int sender = receive(count < 5 ? TIMER : ANY, &m);
        if (sender == TIMER && m.type == PING) {
            Message t = { .type = REQUEST };
            sendrec(TEMP, &t);       /* matching REPLY contains t.value */
            if (count == 5)
                sum -= history[next];
            else
                ++count;
            history[next] = t.value;
            sum += t.value;
            next = (next + 1) % 5;
        } else if (count == 5 && m.type == REQUEST) {
            Message answer = { .type = REPLY, .value = sum / 5.0 };
            send(sender, &answer);
        }
    }
}

Before the fifth reading, selective reception from TIMER prevents premature client requests from being accepted. Such clients wait at their synchronous sends; they are not given a partial arithmetic mean. Thereafter the operating-system process receives both timer messages and client requests. Each accepted PING initiates one measurement; each accepted client request returns the arithmetic mean of the five most recently completed measurements, without initiating another measurement or changing the circular buffer.

The loop invariant is that count is the number of valid readings, capped at five, sum is their sum, and next is the next unused slot during startup or the oldest slot afterwards. Removing the overwritten reading and adding the new one preserves this loop invariant. Each update and reply uses

O (1)

time complexity and

O (1)

storage, since the window length is fixed. Under timely sensor replies, timer delivery and process scheduling, measurements are initiated once per second. The next parts explain failures of these timing assumptions; the code does not promise one-second sampling when the sensor itself cannot sustain it.

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Digital systems, linear algebra, introduction to formal proof resit / 1 / b / Solution 2026-10-25

Use an explicit-stack depth-first tree traversal. Descend the left branch immediately and put each nonempty right subtree on a stack for later. For the same node declarations as in the paper, an original C programming language implementation is:

int sum_iter(tree t)
{
    tree pending[32];
    unsigned top = 0;
    int total = 0;
    while (t != NULL || top != 0) {
        if (t == NULL) {
            t = pending[--top];
        } else {
            total += t->data;
            if (t->right != NULL)
                pending[top++] = t->right;
            t = t->left;
        }
    }
    return total;
}

The loop invariant says that the accumulated labels plus the sums of the current subtree and all pending subtrees equal the original tree sum, with the unvisited subtrees disjoint. Visiting a node adds its label and replaces its subtree by its two children. Popping merely changes which pending subtree is current. When both current and pending subtrees are absent, the invariant proves the result.

At most one unvisited right sibling is pending at each level of the current ancestor path. If depth means the number of nonempty nodes on a longest root-to-leaf path, depth at most 32 requires at most 31 pending right siblings. A 32-word array is therefore sufficient; it also covers the convention that depth counts at most 32 edges. The depth promise makes unchecked pushes valid here. For arbitrary input, a production implementation should check capacity rather than overwrite its frame.

A corresponding Thumb instruction set implementation keeps the total in r4, the array base in r5, and its next-free address in r6:

.global sum_iter_asm
.thumb_func
sum_iter_asm:
    push {r4, r5, r6, lr}
    sub  sp, sp, #128        @ 32 pending pointers
    mov  r5, sp              @ base of pending array
    mov  r6, sp              @ empty stack: next-free equals base
    movs r4, #0
.Lvisit:
    cmp  r0, #0
    beq  .Ltake_pending
    ldr  r1, [r0, #0]
    adds r4, r4, r1          @ consume this node's label
    ldr  r1, [r0, #8]
    cmp  r1, #0
    beq  .Lleft
    str  r1, [r6, #0]        @ defer the nonempty right subtree
    adds r6, r6, #4
.Lleft:
    ldr  r0, [r0, #4]        @ continue down the left branch
    b    .Lvisit
.Ltake_pending:
    cmp  r6, r5
    beq  .Ldone
    subs r6, r6, #4
    ldr  r0, [r6, #0]
    b    .Lvisit
.Ldone:
    movs r0, r4
    add  sp, sp, #128
    pop  {r4, r5, r6, pc}

The stack pointer stays fixed while the array is used; r6 is a separate cursor inside that array. All callee-saved registers touched by the function are restored. Each nonempty node contributes its label exactly once. As in part (a), require that every partial total fits the signed result type; a representable final answer alone does not prevent overflow in a different summation order.

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Imperative programming (resit) / 1 / a / ii / Solution 2026-10-25

Use exponentiation by squaring with the remaining exponent halved on every iteration:

def eaFast(n: Int): Double = {
  require(n > 0)
  var remaining = n
  var base = 1.0 + 1.0 / n.toDouble
  var result = 1.0
  while (remaining > 0) {
    if (remaining % 2 == 1) result *= base
    base *= base
    remaining /= 2
  }
  result
}

Writing

a = 1 + 1/ n

, the exact-arithmetic loop invariant is

re mainin g \geq 0

and

res u lt ba s e^{re mainin g} = a^{n}

. For an even integer exponent

2 q

, replace the base by its square and the exponent by

q

. For an odd integer exponent

2 q + 1

, first multiply the accumulator by the base and then make the same replacement. Both preserve the product. The loop variant is remaining, which strictly decreases while positive. At exit the remaining exponent is zero, so the returned value approximates $(1 + 1/ n)^{n}$ .

There are

L = ⌊ lo g_{2} n ⌋ + 1

iterations,

L

squarings and one accumulator multiplication for each set bit of

n

: between

L + 1

and

2 L

multiplications. Thus the bound is

Θ (lo g n)

n \to \infty

, or

Θ (1 + lo g n)

including the small case

n = 1

. All power variables are Double; no unintended Int squaring occurs.

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Imperative programming (resit) / 1 / a / i / Solution 2026-10-25

Use a Double base so that the reciprocal is not truncated by integer division. Repeated multiplication gives the requested linear-work approximation to Euler's number.

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

In exact arithmetic over the real numbers, the loop invariant is

0 \leq i \leq n

and

res u lt = ba s e^{i}

. It holds initially, one multiplication establishes the next exponent, and at exit

i = n

gives the specified power. The nonnegative loop variant is

n - i

. There are exactly $n$ loop multiplications, hence

Θ (n)

in asymptotic analysis, and one division to form the base. With floating-point arithmetic, the invariant describes the intended exact result; the actual output has the corresponding rounding errors.

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

Maintain the reciprocal factorial term rather than calculating large factorials separately:

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 exact-arithmetic loop invariant is

0 \leq i \leq n

t er m = 1/ i!

, and

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

. It holds for

i = 0

because

0! = 1

. Dividing by the new index produces the next reciprocal factorial; adding it extends the partial sum. The loop variant is

n - i

. At exit the sum includes all terms from $0$ through $n$ , using exactly

n

divisions and no multiplications in the loop. In particular, the initial 1.0 accounts for the zero-index term. The work bound is

O (n)

, with constant auxiliary space.

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

Avoid forming the enormous powers in the original ratios. Put

a = 1 + 1/ n

b = 1 + 1/ (n - 1)

and

k = n - 1

; algebra gives

e_{c} (n) = (n + 1) a a^{k} - n b^{k} .

Use simultaneous exponentiation by squaring to compute the two powers with one loop and a shared remaining exponent:

def ec(n: Int): Double = {
  require(n > 1)
  val dn = n.toDouble
  val a = 1.0 + 1.0 / dn
  val b = 1.0 + 1.0 / (dn - 1.0)
  var remaining = n - 1
  var u = a
  var v = b
  var pa = 1.0
  var pb = 1.0
  while (remaining > 0) {
    if (remaining % 2 == 1) {
      pa *= u
      pb *= v
    }
    u *= u
    v *= v
    remaining /= 2
  }
  ((dn + 1.0) * a) * pa - dn * pb
}

The exact-arithmetic loop invariant is

re mainin g \geq 0

p a u^{re mainin g} = a^{n - 1}

and

p b v^{re mainin g} = b^{n - 1}

. The even integer and odd integer cases preserve both equalities in parallel. The loop variant is remaining. On termination, the displayed expression is exactly the desired approximation in the ideal arithmetic model. For

L = ⌊ lo g_{2} (n - 1)⌋ + 1

, the loop uses at most

4 L

multiplications, followed by three more: $O (lo g n)$ multiplications and one loop.

Converting n to Double before adding one also avoids overflowing n + 1 at Int.MaxValue. The algebra avoids power overflow but does not remove catastrophic cancellation: the final subtraction combines quantities of order

n e

to obtain a result of order

e

. For sufficiently large

n

, floating-point rounding can outweigh the mathematical truncation error. For example, at n == 1000000 this Double computation returns approximately 2.7180521293, although the exact formula is approximately 2.71828182845916. Arbitrarily many requested decimal digits require increased arithmetic precision, not simply a larger Int argument.

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

Without order information, inspect entries one row at a time:

def searchUnordered(f: Array[Array[Int]], x: Int): Option[(Int, Int)] = {
  val n = f.length
  val m = if (n == 0) 0 else f(0).length
  var i = 0
  while (i < n) {
    var j = 0
    while (j < m) {
      if (f(i)(j) == x) return Some((i, j))
      j += 1
    }
    i += 1
  }
  None
}

The outer loop invariant excludes every entry in earlier rows; the inner one also excludes columns before j in the current row. Failed equality tests preserve these exclusions. The inner and outer loop variants are

m - j

and

n - i

, respectively. A successful return identifies an actual match, while exhaustion excludes the entire array. At most

nm

entries are inspected.

The source's “at least

O (nm)

” should be read as a worst-case $Ω (nm)$ lower bound, using the correct asymptotic direction. If any entry were left unread on an all-nonmatching input, changing only that entry to

x

would leave the observations identical while changing the answer. Thus every always-correct procedure needs

nm

inspections in the worst case, and this algorithm achieves

Θ (nm)

entry inspections. Empty dimensions return absence; the asymptotic claim concerns nonempty arrays.

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Imperative programming (resit) / 2 / c / Solution 2026-10-25

Use a lower-bound search separately in each nondecreasing row:

def searchRows(f: Array[Array[Int]], x: Int): Option[(Int, Int)] = {
  val n = f.length
  val m = if (n == 0) 0 else f(0).length
  if (m == 0) return None
  var i = 0
  while (i < n) {
    var lo = 0
    var hi = m
    while (lo < hi) {
      val mid = lo + (hi - lo) / 2
      if (f(i)(mid) < x) lo = mid + 1
      else hi = mid
    }
    if (lo < m && f(i)(lo) == x) return Some((i, lo))
    i += 1
  }
  None
}

The outer loop invariant says there is no match in earlier rows. The inner invariant is

0 \leq l o \leq hi \leq m

, with every value before lo smaller than

x

and every value from hi onward at least

x

. Sortedness justifies each exclusion, and hi - lo strictly decreases. At exit, a match in this row exists exactly when the lower-bound index is inside the row and holds

x

. Failure extends the outer exclusion.

The cost is $O (n (1 + lo g m))$ , conventionally written

O (n lo g m)

for

m \geq 2

; the extra one matters when a row has a single entry. Storage is constant. The source's column ranges must use indices strictly below

m

, since f(i)(m) is outside the array.

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Imperative programming (resit) / 2 / e / Solution 2026-10-25

Maintain a remaining rectangle with its top-right corner at (i,j):

def searchMonotone(f: Array[Array[Int]], x: Int): Option[(Int, Int)] = {
  val n = f.length
  val m = if (n == 0) 0 else f(0).length
  var i = 0
  var j = m - 1
  while (i < n && j >= 0) {
    val v = f(i)(j)
    if (v == x) return Some((i, j))
    else if (v < x) i += 1
    else j -= 1
  }
  None
}

The loop invariant is that any match must lie in rows

i, \dots, n - 1

and columns

0, \dots, j

. Smaller corner values exclude the current row, larger ones exclude the current column, as shown in part (d). The loop variant

(n - i) + (j + 1)

is nonnegative while the rectangle is nonempty and decreases by one on every unsuccessful inspection. When the loop exits, the rectangle is empty, so absence is established.

At most $n + m - 1$ entries are inspected when both dimensions are positive, giving

O (n + m)

running time and

O (1)

auxiliary space. An empty dimension causes no entry access. Duplicates do not affect the argument, since every exclusion uses a strict inequality relative to the target.

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Imperative programming (resit) / 4 / f / Solution 2026-10-25

Append nonzero entries in increasing index order; repeatedly calling setElement would unnecessarily rescan earlier entries and could make construction quadratic.

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

The loop invariant says that the list represents exactly the nonzero entries of the processed input prefix, in their original coordinate order, and tail is the final node or the header when none exist. Every append preserves the cycle and ordering. At exit, all input coordinates have their intended values. Construction takes $O (n)$ time and $O (k)$ data nodes, where

n

is the array length and

k

the number of nonzeros, plus one header. The input array is unchanged.

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Imperative programming (resit) / 4 / g / Solution 2026-10-25

Use sparse dot product by merging indices: only equal coordinate indices can contribute, so merge the two increasing index streams:

def dotProduct(vec1: Node, vec2: Node): Double = {
  require(vec1 != null && vec2 != null)
  require(vec1.index == vec2.index, "dimension mismatch")
  var p = vec1.next
  var q = vec2.next
  var answer = 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 {
      answer += p.value * q.value
      p = p.next
      q = q.next
    }
  }
  answer
}

The loop invariant states that the accumulator contains all common-coordinate products already passed, while no unprocessed smaller coordinate can acquire a future partner. If one current index is smaller, the other list has no remaining entry at that index, so its product is zero. Equal indices add their product and advance both. Once either list ends, all remaining coordinates of the other have zero partners.

Thus the code computes the dot product in coordinate order, subject to floating-point rounding, using $O (k_{1} + k_{2})$ time and constant auxiliary storage. It does not scan implicit zeros or alter either vector, and it also handles both arguments referring to the same header.

Past exam of the year 1 of the computer science course of the University of Oxford / 2023 / Functional programming, design and analysis of algorithms / 6 / b / Solution 2026-10-25

Sort the open intervals by increasing left endpoint. Scan them in that order, maintaining the largest right endpoint

R

among previously seen intervals. For the next interval

(a, b)

, report an intersection if $a < R$ ; otherwise set

R = max (R, b)

and continue. Equality is allowed:

(a, R)

and

(R, b)

do not meet because the intervals are open. For zero or one interval, return that they are mutually non-intersecting.

a < R

, a previous interval with right endpoint

R

has left endpoint at most

a

and has positive length. Together with

b > a

, this guarantees an interior common point. Conversely, if

a \geq R

, every earlier interval ends at or before

a

, so none intersects the new one. This loop invariant proves correctness. A comparison sort costs

O (n lo g n)

time and the scan costs

O (n)

For the lower bound, transform an input of integers

z_{1}, \dots, z_{n}

for the element distinctness problem into

r_{i} = (2 z_{i}, 2 z_{i} + 1) .

Equal integers produce identical, intersecting intervals. Unequal integers differ by at least one, so their intervals are disjoint. The answer therefore decides whether all the integers are distinct. Moreover, comparing any two constructed endpoints can be simulated by comparing their original integers and, only on equality, their fixed offsets

0

1

. Thus the transformation preserves the comparison model, rather than gaining extra information from arithmetic on arbitrary endpoints. The supplied distinctness lower bound gives $Ω (n lo g n)$ comparisons, matching the upper bound. This is the comparison lower bound for interval disjointness.

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

A loop invariant is a property of the program state that holds whenever control reaches the loop's condition, including the final failed test. Its main purpose is proving partial correctness: establish it initially, prove one guarded iteration preserves it, then combine it with the negated condition to obtain the postcondition. A separate loop variant or another progress argument proves algorithm termination and hence total correctness.

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

The proposed condition is not a loop invariant at the loop head. It holds initially and on entry to every executed body, but the iteration starting with i == 10 finishes with i == 11. Control then returns to the condition with the proposed upper bound false. A suitable numerical loop invariant is $1 \leq i \leq 11$ . If the number of printed lines matters, strengthen it to “exactly

i - 1

lines have been printed.” At exit, this and i > 10 give exactly ten printed lines. The nonnegative loop variant

11 - i

decreases by one on every iteration.

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

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 is

0 \leq l o \leq hi \leq N, (\forall k < l o) a (k) < x, (\forall k \geq hi, k < N) a (k) \geq x .

Initially the excluded prefix and suffix are empty, so both quantified assertions hold. During an iteration,

l o \leq m_{1} \leq m_{2} < hi

. If

a (m_{1}) \geq 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 \leq 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 = ⌊ d /3 ⌋

, the three possible new lengths are

q, q, d - 2 q - 2

, with the middle branch feasible only when nonnegative; each is at most

⌊ d /3 ⌋

. 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 (lo g (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.

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

Search only the suffix strictly after each candidate first index. This enforces distinct indices even when the target is twice an existing value. Compute the complement in Long to prevent integer overflow: subtracting two Int values can require 33 signed bits.

def twoSum(a: Array[Int], target: Int): (Int, Int) = {
  def lowerBound(from: Int, wanted: Long): Int = {
    var lo = from
    var hi = a.length
    while (lo < hi) {
      val mid = lo + (hi - lo) / 2
      if (a(mid).toLong < wanted) lo = mid + 1
      else hi = mid
    }
    lo
  }
  var i = 0
  while (i < a.length - 1) {
    val wanted = target.toLong - a(i).toLong
    val j = lowerBound(i + 1, wanted)
    if (j < a.length && a(j).toLong == wanted) return (i, j)
    i += 1
  }
  (0, 0)
}

The outer loop invariant says that no solution has a smaller first index than i, when a pair is written in increasing index order. A failed suffix binary search proves there is no partner for the current i, extending the excluded prefix by one. A successful return has

j > i

and

a (j) = t - a (i)

in exact integer arithmetic. At exhaustion, every possible ordered pair has been excluded, so the sentinel (0,0) means no solution. The inner loop invariant is the standard lower-bound partition, restricted to the suffix starting at i + 1.

There are at most

N - 1

suffix searches, each taking

O (lo g (N + 1))

running time, so the total is

O (N lo g (N + 1))

, customarily written

O (N lo g N)

for

N \geq 2

. Auxiliary space is

O (1)

. Empty and singleton arrays immediately return the sentinel. This is distinct-index two-sum by suffix lower bounds; a faster two-pointer technique is also possible on a sorted array, but the code here directly meets the requested search-based bound.

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

Under exact integer arithmetic, the intended result is $⌈ lo g_{2} x ⌉$ , using the ceiling function. A sufficient loop invariant is

i \geq 0, y = 2^{i}, i = 0 \lor 2^{i - 1} < x .

Initially

i = 0, y = 1

, and the final disjunction is true. If the guard holds, the old value

y = 2^{i}

is below

x

. Incrementing i and doubling y therefore preserves

y = 2^{i}

and makes the new lower bound

2^{i - 1} < x

true. At exit

y \geq x

. If

i = 0

, positivity of

x

forces

x = 1

; otherwise

2^{i - 1} < x \leq 2^{i}

. Both cases establish the claimed postcondition. Doubling eventually reaches or exceeds any fixed positive

x

, proving algorithm termination in this arithmetic model. This is the doubling-loop ceiling logarithm argument.

The printed Scala implementation is not correct for its entire stated Int domain. Its y is an Int. For

x > 2^{30}

, it reaches

y = 2^{30}

, wraps to

- 2^{31}

on the next doubling, then becomes zero and stays zero. The guard remains true forever. The loop invariant above is valid for the printed code only when

1 \leq x \leq 2^{30}

. Scala documents Int as a signed 32-bit value equivalent to Java's primitive int.^[ref]

A corrected implementation for every positive Int input widens the doubling variable before any multiplication:

def ceilingLog2(x: Int): Int = {
  require(x > 0)
  var i = 0
  var y = 1L
  while (y < x.toLong) {
    i += 1
    y *= 2L
  }
  i
}

Now at most 31 iterations are needed and

y \leq 2^{31}

, safely within Long. The same loop invariant proves total correctness without the overflow gap.

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

The algorithmic intention is exponentiation by squaring to compute $x^{n}$ for $n \geq 0$ . With exact arithmetic, its loop invariant is

i \geq 0, res u lt y^{i} = x^{n} .

Initially result = 1, y = x, and i = n. For an even integer

i = 2 q

, squaring y and replacing i by

q

preserves the product. For an odd integer

i = 2 q + 1

, first multiply result by y; then

(res u lt y) (y^{2})^{q} = res u lt y^{2 q + 1}

. The nonnegative loop variant i decreases by halving whenever positive. At exit

i = 0

, so the loop invariant yields result = x^n. There are

O (lo g (n + 1))

multiplication steps.

Two qualifications are essential for the actual source. There is no requirement that n be nonnegative: for every n <= 0 the printed function simply returns 1.0. Also, var y = x infers Int, so y *= y uses wrapping integer arithmetic, while the accumulator uses floating-point arithmetic. For example, anotherfunc(50000, 2L) returns -1794967296.0, rather than 2500000000.0. An exact-power loop invariant cannot prove a false claim about that execution.

More precisely, for positive n, after

k

iterations the remaining exponent is

⌊ n / 2^{k} ⌋

, and the Int base is the signed 32-bit representative of

x^{2^{k}}

modulo

2^{32}

. The accumulator multiplies those signed representatives for the set bits of n, in increasing bit order, with a floating-point rounding after each multiplication. This describes the actual code even when the intended power law fails. In an exact implementation, use a nonnegative-exponent precondition and arbitrary-precision integers, for example:

def powerExact(x: Int, n: Long): BigInt = {
  require(x > 0 && n >= 0)
  var result = BigInt(1)
  var y = BigInt(x)
  var i = n
  while (i > 0) {
    if (i % 2 == 1) result *= y
    y *= y
    i /= 2
  }
  result
}

The displayed loop invariant applies exactly to this version. It performs logarithmically many arbitrary-precision multiplications; their bit cost grows with operand size, so that statement is not an

O (lo g n)

bit-complexity bound. Merely making the accumulator a Double does not widen the separate Int base variable.