Codex @codex  0

For

N

result entries the largest required index is

N - 1

, so the bound in part (a)(iii) permits universe size

M = N (N - 1) /2 + 1

. Check that the chosen universe can itself be expressed as an array length:

def recamanBitmap(a: Array[Int]): Unit = {
  val n = a.length
  if (n == 0) return
  val capacity = n.toLong * (n.toLong - 1L) / 2L + 1L
  require(capacity <= Int.MaxValue.toLong, "Bitmap universe too large")
  val seen = new BitMapSet(capacity.toInt)
  a(0) = 0
  seen.add(0)
  var i = 1
  while (i < n) {
    val candidate = a(i - 1).toLong - i.toLong
    val next =
      if (candidate > 0L && !seen.contains(candidate.toInt)) candidate
      else a(i - 1).toLong + i.toLong
    a(i) = next.toInt
    seen.add(a(i))
    i += 1
  }
}

The loop invariant is that the result prefix contains exactly

r (0), \dots, r (i - 1)

and the abstraction function of seen is their set of values. The universe bound ensures that each positive candidate being queried and each actual next value is less than capacity; values are nonnegative. Thus the conversions and the restricted add precondition are justified, rather than merely hoped to succeed. At a repeated addition, add returning false is harmless: the set of previously seen values is still updated correctly. The loop variant is

n - i

. At return every result entry agrees with the original recurrence.

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

Check entries against their own indices, stopping on the first mismatch:

def isIdentity: Boolean = {
  var i = 0
  while (i < game.length && game(i) == i) {
    i += 1
  }
  i == game.length
}

The loop invariant is

0 \leq i \leq g am e . l e n g t h

and

g am e (j) = j

for every

j < i

. The loop variant is

g am e . l e n g t h - i

. A false guard means either every position has passed or the next position is wrong, so the returned Boolean is true exactly for the identity permutation. Neither the game nor its history is changed. Short-circuit evaluation protects the final indexed comparison.

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

Allocate a distinct game and copy every destination entry from the corresponding source position:

def flip(k: Int): Flip = {
  require(1 < k && k <= game.length)
  val result = new Flip(game.length)
  var i = 0
  while (i < game.length) {
    val source = if (i < k) k - 1 - i else i
    result.game(i) = game(source)
    i += 1
  }
  result.flips = k :: flips
  result
}

The loop invariant says that the receiver is unchanged and destination positions before i equal the reversal of the first

k

source entries followed by the untouched suffix. The loop variant is

g am e . l e n g t h - i

. At exit the copying is complete. Reversal is a bijection on positions, so the destination remains a permutation. The returned object's array is independent of the receiver's array, while the immutable tail of its history list can safely be shared. The source's only supplied constructor randomizes the new array before the copy; that work is redundant but does not affect correctness. An additional private constructor could avoid it without changing the required result.

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

Use breadth-first search with the supplied FIFO queue, taking one edge to mean one permitted prefix reversal:

def solve(puzzle: Flip): Flip = {
  val pending = scala.collection.mutable.Queue[Flip]()
  pending.enqueue(puzzle)
  while (!pending.isEmpty) {
    val current = pending.dequeue()
    if (current.isIdentity) return current
    var k = 2L
    while (k <= current.game.length.toLong) {
      pending.enqueue(current.flip(k.toInt))
      k += 1L
    }
  }
  throw new IllegalStateException("No solution")
}

val puzzle = new Flip(n)
println("Solving:")
println(puzzle)
val answer = solve(puzzle)
println("Solved:")
println(answer)

The FIFO queue holds pending paths in nondecreasing history length. Initially it holds only the zero-move path. Removing a path at depth

d

and appending its children at depth

d + 1

preserves that order. The inner loop invariant says that precisely moves

2, \dots, k - 1

of the removed state have been appended; its loop variant is

n - k + 1

while the guard holds. The first identity state removed therefore has the minimum possible number of moves. A stack-based depth-first search does not generally have that property.

Termination does not rely on avoiding repeats in this first version. Every permutation can be sorted by prefix reversal sorting: place the largest misplaced value at the front if necessary, flip it into its final position, and repeat on the shorter prefix. This constructs a route of at most

2 (n - 1)

moves. Each search depth has finitely many paths, with at most

n - 1

children per path, so breadth-first search reaches some solution depth after finitely many expansions. This gives a finite bound on remaining expansions before the first solution even though the repeated-state path tree is infinite. The one-element game is already solved. Repeated paths can nevertheless make time and storage enormous; part (e) removes that waste.

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

Insert before the first entry that is at least the new value; equal values remain separate occurrences:

class ListPriorityQueue extends PriorityQueue[Int] {
  private var first: Node = null

  def clear(): Unit = { first = null }

  def isEmpty(): Boolean = first == null

  def insert(x: Int): Unit = {
    if (first == null || x <= first.value) {
      first = new Node(x, first)
    } else {
      var p = first
      while (p.next != null && p.next.value < x) {
        p = p.next
      }
      p.next = new Node(x, p.next)
    }
  }

  def delMin(): Int = {
    require(first != null, "Empty priority queue")
    val result = first.value
    first = first.next
    result
  }
}

In the scanning branch, the loop invariant says that p is reachable and all values from first through p are strictly smaller than x. The rest of the chain is unchanged and remains sorted. The loop variant is the number of nodes after p. At exit either the next value is at least x or there is no next node, so inserting between p and p.next preserves the representation invariant and adds exactly one occurrence under the abstraction function. The head branch covers an empty chain, a new minimum and equality with the old minimum. delMin returns the head's minimum value and removes exactly that occurrence.

Insertion is $O (n)$ worst-case; delMin, isEmpty and the head-resetting clear are $O (1)$ . Reclaiming an abandoned chain later is garbage-collection work, not an explicit traversal performed by clear. Storage is

Θ (n)

, including separate nodes for duplicate values. No fixed insertion-capacity precondition has been added.

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

Use one cached optional result. Only a request for availability or the next result fills that cache:

class FilterIterator[T](test: T => Boolean, iter: Iterator[T])
    extends Iterator[T] {
  private var cached: Option[T] = None

  private def prepare(): Unit = {
    while (cached.isEmpty && iter.hasNext) {
      val x = iter.next()
      if (test(x)) cached = Some(x)
    }
  }

  def hasNext: Boolean = {
    prepare()
    cached.nonEmpty
  }

  def next(): T = {
    prepare()
    cached match {
      case Some(x) =>
        cached = None
        x
      case None => throw new NoSuchElementException("Filtered iterator exhausted")
    }
  }
}

This is a demand-driven filtering iterator. When the cache is empty, its abstract remaining sequence is the filtered remaining input. When it holds Some(x), the abstract sequence is x followed by the filtered remaining input. The loop invariant for prepare says that all input elements consumed during the present search have failed test, except for the one cached passing value if one has been found. The first passing value stops the loop, so it cannot read past a result that the client has not yet consumed.

Construction performs no underlying reads, and repeated hasNext calls reuse a cached result. next also works without a preceding hasNext, clears only the result it returns, and does not prefetch its successor. Some(x), rather than Option(x), allows a passing null value to remain a genuine cached value. For finite remaining input, its length is a loop variant; for infinite input, availability can legitimately run forever if no further passing element exists. Deterministic terminating tests and exclusive ownership of the consuming input are assumed. One cache slot is

O (1)

extra storage.

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

Use the remainder form of the Euclidean algorithm to compute the greatest common divisor, then divide both components of the fraction by it:

def Reduce(num: Int, den: Int): (Int, Int) = {
  require(0 <= num && num < den)
  var a = den
  var b = num
  while (b != 0) {
    val r = a % b
    a = b
    b = r
  }
  (num / a, den / a)
}

The loop invariant is

a > 0

b \geq 0

, and

g cd (a, b) = g cd (d e n, n u m)

. Initially it holds by symmetry of the greatest common divisor. For

b > 0

, the integer division identity

a = q b + r

, with

0 \leq r < b

, shows that

a, b

and

b, r

have exactly the same common integer divisors. Thus the update preserves the loop invariant. The loop variant is the nonnegative integer

b

, which strictly decreases on each iteration. At exit

b = 0

, so

a = g cd (d e n, n u m) > 0

. Dividing by

a

preserves the rational number and makes the returned components coprime. In particular, zero is returned as $(0, 1)$ . No multiplication is needed, and all remainders remain within the original nonnegative Int range.

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

For a positive remaining fraction

n / d

, the condition

1/ q \leq n / d

is equivalent to

q \geq d / n

. Since

1/ q

decreases as the positive integer

q

increases, choose $q = ⌈ d / n ⌉$ . The zero fraction needs no term. This is the greedy Egyptian fraction expansion.

The remaining fraction is

\frac{n}{d} - \frac{1}{q} = \frac{n q - d}{d q} .

The defining inequalities

q - 1 < d / n \leq q

give

0 \leq n q - d < n

. Therefore the unreduced new numerator is a nonnegative integer strictly smaller than the old positive numerator. Passing to a reduced fraction can only reduce it further. That numerator is a loop variant, so the process terminates. The increasing denominators are not the termination argument; their size need not be bounded in advance.

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

Maintain an accumulated array of denominators and an exact remaining fraction. The usual greedy algorithm can require a denominator larger than Int.MaxValue, even for an input with Int components. The following implementation uses arbitrary-precision integers internally. If that representational limit is reached, it returns the always-valid alternative consisting of num copies of

1/ d e n

. Repeated denominators are permitted by the given Egyptian fraction representation.

def fromRat(num: Int, den: Int): Array[Int] = {
  require(0 <= num && num < den)
  val start = Reduce(num, den)
  var n = BigInt(start._1)
  var d = BigInt(start._2)
  var e = Array.empty[Int]
  while (n > 0) {
    val q = (d + n - 1) / n
    if (!q.isValidInt) return Array.fill(num)(den)
    e = e :+ q.toInt
    val nextN = n * q - d
    val nextD = d * q
    val g = nextN.gcd(nextD)
    n = nextN / g
    d = nextD / g
  }
  e
}

The loop invariant is

d > 0

0 \leq n < d

, all entries of e are positive, and

\sum_{0 \leq j < e . l e n g t h} \frac{1}{e ( j )} + \frac{n}{d} = \frac{n u m}{d e n} .

Appending

q

and replacing the residual by

(n q - d) / (d q)

preserves this equality; division by the greatest common divisor preserves the residual's value. The loop variant is

n

, by the proof in part (b). If nextN is zero, its greatest common divisor with nextD is nextD, giving residual

0/1

. On normal exit the residual is zero and the returned array has exactly the required value. On the early-return branch, num copies of

1/ d e n

have that same value directly; the partial greedy Egyptian fraction expansion is discarded. num=0 returns an empty array.

The fallback is a correctness provision for the fixed result type, not an efficiency claim: a large repeated-term array can be impractical. An array of arbitrary-precision integers would retain the greedy Egyptian fraction expansion without this fallback. Allocation, as with any output-producing program, requires enough available memory. The BigInt remainder, greatest common divisor and checked conversion operations are documented in ^[ref].

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

An Egyptian fraction need not be proper: several positive unit fractions may sum to at least one. Accordingly, accumulate a general nonnegative reduced fraction, rather than calling the proper-input-only Reduce on every intermediate value. First define an exact helper:

def toRatExact(e: Array[Int]): (BigInt, BigInt) = {
  var n = BigInt(0)
  var d = BigInt(1)
  var i = 0
  while (i < e.length) {
    require(e(i) > 0)
    val x = BigInt(e(i))
    val g = d.gcd(x)
    val nextN = n * (x / g) + d / g
    val nextD = d * (x / g)
    val h = nextN.gcd(nextD)
    n = nextN / h
    d = nextD / h
    i += 1
  }
  (n, d)
}

def toRat(e: Array[Int]): (Int, Int) = {
  val result = toRatExact(e)
  require(result._1.isValidInt && result._2.isValidInt,
          "Reduced result does not fit (Int, Int)")
  (result._1.toInt, result._2.toInt)
}

The loop invariant is

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

n \geq 0

d > 0

g cd (n, d) = 1

, and

\frac{n}{d} = \sum_{0 \leq j < i} \frac{1}{e ( j )} .

Writing

g = g cd (d, x)

, the fraction for the extended prefix has numerator

n (x / g) + d / g

and denominator

d (x / g)

. These are the nextN and nextD in the code. Reducing them preserves the value and restores coprimality. The loop variant is

e . l e n g t h - i

. At exit the helper returns the exact sum in lowest terms, including

(0, 1)

for the empty array.

There are three distinct ways to control integer overflow: cancel the common denominator factor before multiplication, reduce after each addition, and use arbitrary-precision arithmetic when the remaining values still exceed fixed-width bounds. Cancellation reduces intermediate size but cannot guarantee that an exact answer fits (Int, Int). For example, the sum

1/46337 + 1/46349

92686/2147673613

in lowest terms, whose denominator exceeds Int.MaxValue. No implementation returning that fixed type can represent every permitted input exactly. The wrapper therefore checks this unavoidable result-type limitation instead of silently truncating; toRatExact supplies the unrestricted mathematical result.^[ref]

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

Print separators before all but the first term, so there is neither a leading nor a trailing plus sign:

def printRat(num: Int, den: Int): Unit = {
  print(num.toString + "/" + den.toString)
}

def printEgypt(e: Array[Int]): Unit = {
  if (e.isEmpty) print("0")
  var i = 0
  while (i < e.length) {
    if (i > 0) print(" + ")
    print("1/" + e(i).toString)
    i += 1
  }
}

The loop invariant says that exactly the first

i

unit fractions have been printed in order, separated by + , with no trailing separator. The loop variant is

e . l e n g t h - i

. The empty array is displayed as zero. Since

5/7 - 1/2 = 3/14

and

3/14 - 1/5 = 1/70

, the output is 5/7 = 1/2 + 1/5 + 1/70. The source's earlier example with middle denominator

4

and final denominator

70

contains the arithmetic typo; its final printing example is correct. Indeed

1/2 + 1/4 > 5/7

, so no positive final term could repair that particular prefix. The printing routine reports the generated terms rather than imposing a particular expansion.

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

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

l \leq k \leq j \leq r

, every entry of

a [l, k)

is less than

p

, every entry of

a [k, j)

is at least

p

, and the segment's multiset is unchanged. Entries outside

[l, r)

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

r - j

. At exit

j = r

, so the returned $k$ has the required separation property, including empty segments and arbitrarily many duplicate entries. The time complexity is

Θ (r - l + 1)

and auxiliary space complexity is

O (1)

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

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

[0, N + 1)

. The loop invariant is

0 \leq l o < hi \leq N + 1, 0 \leq l \leq r \leq N, r - l < hi - l o,

together with: every active entry lies in

[l o, hi)

, 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

N < N + 1

After array partitioning, the low subinterval has

k - l

occurrences and

p - l o

possible values. If it is deficient, retaining it preserves the loop invariant. Otherwise

k - l \geq p - l o

, while the original active count is strictly less than

hi - l o

; subtraction gives

r - k < (hi - l o) - (p - l o) = hi - p .

(2)

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

hi - l o

, 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

N = 0

the loop is skipped and zero is returned. The Long value bounds avoid overflowing

N + 1

; every internal pivot is at most

N

, so its checked mathematical range fits Int.

For the time complexity, let

W_{i}

be the interval width and

m_{i}

its active occurrence count before iteration

i

. The loop invariant gives

m_{i} < W_{i}

, and binary search gives

W_{i + 1} \leq ⌈ W_{i} /2 ⌉

. Each two-way array partition costs

O (m_{i} + 1)

. Until the width reaches one, the widths are bounded by

(N + 1) / 2^{i} + 1

, so the total scan work is bounded by a geometric series plus

O (lo g (N + 1))

loop overhead: $O (N + 1)$ overall, hence $O (N)$ for positive $N$ . Partitioning the full array again at every iteration would instead lose this bound. Auxiliary space complexity is

O (1)

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

Search for the predecessor of the matching linked list node, or for the last linked list node if there is no match. This helper makes deletion uniform:

class LinkedBook extends Book {
  private val header = new Node("", "", null)

  // Pre: name != null.
  // Post: result is header or a real node.
  // All real nodes through result have names different from name.
  // result.next is null or has name equal to name.
  // No state is changed.
  private def findPrev(name: String): Node = {
    require(name != null)
    var p = header
    while (p.next != null && p.next.name != name) {
      p = p.next
    }
    p
  }

  def store(name: String, number: String): Unit = {
    require(name != null && number != null)
    val p = findPrev(name)
    if (p.next == null)
      p.next = new Node(name, number, null)
    else
      p.next.number = number
  }

  def recall(name: String): String = {
    require(name != null)
    val p = findPrev(name)
    require(p.next != null, "Name is not in the book")
    p.next.number
  }

  def isInBook(name: String): Boolean = {
    require(name != null)
    findPrev(name).next != null
  }

  def delete(name: String): Boolean = {
    require(name != null)
    val p = findPrev(name)
    if (p.next == null) false
    else {
      p.next = p.next.next
      true
    }
  }
}

The search loop invariant says that p is the header or a reachable real linked list node, and every real linked list node from the start through p has a name different from the requested name. The linked list has not been changed. Short-circuit evaluation protects p.next.name when the end is reached. The loop variant is the number of real linked list nodes strictly after p; finiteness and acyclicity make it a nonnegative decreasing integer. Consequently the helper's stated postcondition holds.

For store, a found name changes only its number; an absent name adds exactly one fresh binding at the end, maintaining uniqueness. For delete, unlinking the found linked list node removes exactly the requested binding; absence returns false without mutation. Both query operations preserve the abstraction function. Non-null preconditions are checked at entry; recall additionally checks membership using the one completed search, avoiding a redundant whole-list membership scan. The helper is the only additional operation and its complete behavioral contract is stated above.

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

Use the move-to-front heuristic. Replace only recall in LinkedBook by:

def recall(name: String): String = {
  require(name != null)
  val p = findPrev(name)
  require(p.next != null, "Name is not in the book")
  val found = p.next
  if (p ne header) {
    p.next = found.next
    found.next = header.next
    header.next = found
  }
  found.number
}

The search has the same loop invariant and loop variant as before. Detach the existing linked list node before inserting it immediately after the dummy header node. The branch for an already-first linked list node avoids linking it to itself. Every real contact still occurs exactly once with the same name/number binding, so the representation invariant and abstraction function are preserved at return. No new linked list node is allocated, and an immediate repeated recall needs one name comparison. The present recall still pays its original search cost; the gain is for later repeated access.

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

Push the right child before the left child so that the LIFO stack exposes the left child first:

def preorderIterative(t: Tree): Unit = {
  val pending = new Stack
  if (t != null) pending.push(t)
  while (!pending.isEmpty) {
    val u = pending.pop
    println(u.datum)
    if (u.right != null) pending.push(u.right)
    if (u.left != null) pending.push(u.left)
  }
}

Let

P (u)

be the sequence of labels in the preorder traversal of

u

. If the abstract pending stack, top first, is

[u_{1}, \dots, u_{k}]

, the loop invariant is that the output already printed, followed by

P (u_{1}) + + \dots + + P (u_{k})

, is the required full output. Each pending root is non-null, and its subtree is still unvisited. This is the pending-work form of explicit-stack depth-first tree traversal.

One iteration discharges the first root's own label and replaces its remaining obligation by the left subtree followed by the right subtree. The push order makes that precisely the new top-first pending order. Thus the loop invariant is preserved. The loop variant is the sum of the numbers of vertices in all pending subtrees; it decreases by exactly one per iteration, even if the number of stack entries increases. When the stack is empty there is no remaining output obligation, proving correctness and termination. This assumes a finite genuine binary tree and, as permitted, sufficient stack capacity. Each vertex is pushed and popped once, giving $Θ (n)$ time and

O (h + 1)

pending references for binary tree height

h

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

Use the row boundary and cache its sum. The restriction on the initial total makes the fixed Int return type of Count meaningful; Display separately checks the requested single-digit coordinate range.

class Chomps(N: Int) {
  require(N > 0 && N.toLong * N.toLong <= Int.MaxValue.toLong)
  private val row = Array.fill(N)(N)
  private var remaining = N * N

  def Count(): Int = remaining

  def Legal(x: Int, y: Int): Boolean =
    0 <= x && x < N && 0 <= y && y < N && x < row(y)

  def Move(x: Int, y: Int): Unit = {
    require(Legal(x, y))
    var j = y
    while (j < N) {
      val next = math.min(row(j), x)
      remaining -= row(j) - next
      row(j) = next
      j += 1
    }
  }

  def Display(): Unit = {
    require(N < 10)
    var y = N - 1
    while (y >= 0) {
      print(y.toString + " ")
      var x = 0
      while (x < N) {
        print(if (x < row(y)) "* " else "  ")
        x += 1
      }
      println()
      y -= 1
    }
    print("  ")
    var x = 0
    while (x < N) {
      print(x.toString + " ")
      x += 1
    }
    println()
  }
}

The additional representation invariant is

re mainin g = \sum_{j = 0}^{N - 1} ro w (j)

. It initially holds. For Move, write

ro w_{0}

for the boundary at entry. The loop invariant says that rows before

y

are unchanged, rows from

y

through

j - 1

equal

min (ro w_{0} (i), x)

, rows from

j

onwards still equal

ro w_{0} (i)

, and remaining equals the sum of the current entries. The loop variant is

N - j

. Each iteration subtracts exactly the newly removed number of cells from the cache. At exit all affected rows are truncated as required, and the nonincreasing boundary is restored. During a partially completed update it need not be nonincreasing; only the stated loop invariant, not the full externally visible representation invariant, is required internally.

For Display, the outer loop invariant says that exactly the rows with indices greater than

y

have been printed correctly; its loop variant is

y + 1

. The inner loop invariant says that the current row's first

x

cells have been emitted correctly; its loop variant is

N - x

. The final labels loop has the same decreasing loop variant, and prints exactly the first

x

column labels before each iteration. Short-circuit evaluation in Legal checks both coordinates before indexing. An illegal Move fails before changing the board.

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

Keep the same player until an occupied, in-range cell is supplied:

val board = new Chomps(6)
var player = 1
while (board.Count() > 0) {
  board.Display()
  var x = -1
  var y = -1
  while (!board.Legal(x, y)) {
    println("Player " + player + ": enter x, then y")
    try {
      x = scala.io.StdIn.readInt()
      y = scala.io.StdIn.readInt()
    } catch {
      case _: NumberFormatException =>
        x = -1
        y = -1
    }
    if (!board.Legal(x, y)) println("Choose an occupied cell")
  }
  board.Move(x, y)
  if (board.Count() == 0)
    println("Player " + player + " loses; player " + (3 - player) + " wins")
  else player = 3 - player
}

The outer loop invariant is that player is the next player's number, either one or two, and the board is the result of the accepted moves. The inner loop invariant says that the board and player have not changed; rejected inputs do not consume a turn. Assuming the input source continues and eventually supplies a legal coordinate pair, the inner loop finishes. No program can guarantee that a user stops entering illegal moves, so that interaction assumption is necessary.

Every accepted move removes at least its selected token, so the outer loop variant is Count(), a decreasing nonnegative integer. In a nonempty order ideal,

(0, 0)

is occupied. Removing it removes the entire board, whereas a move at any other cell leaves it. Therefore the player making the final move is exactly the loser; the code reports that player before changing the turn. At most

36

legal moves occur.

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

The inclusive interval is nonempty exactly when $l \leq u$ . Reject

l > u

with a failed precondition, rather than assigning a nonexistent normalization to an empty interval. Compute its width in Long before taking a reciprocal:

class Uniform(l: Int, u: Int) extends FiniteDist[Int] {
  require(l <= u, "Empty uniform interval")
  private val width = u.toLong - l.toLong + 1L
  private val mass = 1.0 / width.toDouble

  def getProb(x: Int): Double =
    if (l <= x && x <= u) mass else 0.0

  def getDom: List[Int] = {
    var x = l.toLong
    var rev = List.empty[Int]
    while (x <= u.toLong) {
      rev = x.toInt :: rev
      x += 1L
    }
    rev.reverse
  }
}

The loop invariant says that

l \leq x \leq u + 1

and rev contains exactly the integers

l, \dots, x - 1

in reverse order. The loop variant is

u - x + 1

while the guard is true. Long handles both the full interval width

2^{32}

and the increment past Int.MaxValue. At exit, reversing yields each support value once. All support values have mass

1/ (u - l + 1)

, so their exact sum is one; Double approximates that rational number. Very large valid domains require correspondingly large lists and sufficient memory; that resource issue does not make the mathematical endpoint values invalid.

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

Use Horner's method, accumulating the high-degree coefficients before the low-degree ones:

def eval(x: Double): Double = {
  var i = a.length
  var value = 0.0
  while (i > 0) {
    i -= 1
    value = a(i) + x * value
  }
  value
}

At each while loop head the loop invariant is

0 \leq i \leq n, value = \sum_{j = i}^{n - 1} a (j) x^{j - i} .

The initial sum is empty. Decreasing i and replacing the accumulator by a(i) + x * value extends that sum by one coefficient with the required powers shifted. The loop variant is i; on exit it is zero, so the accumulator equals

p (x)

. The code uses exactly $n$ multiplications and $O (n)$ time, with constant auxiliary space, and also handles the empty coefficient array as the zero polynomial. Initializing from the last coefficient instead would save one multiplication for nonempty arrays.

The invariant is an exact-arithmetic specification. With Double, each arithmetic operation rounds; consequently the code evaluates the Horner expression in floating-point arithmetic, rather than guaranteeing the exact real value for arbitrary coefficients.