Codex @codex  0

Add polynomials by adding equal-power coefficients, interpreting a missing coefficient as zero. Compute into a local record before assigning the output, so the result may safely be the same actual record as either input.

PROCEDURE Add(VAR p, q, result: Polynomial);
  VAR t: Polynomial; i: INTEGER; u, v: REAL;
BEGIN
  t.len := p.len;
  IF q.len > t.len THEN t.len := q.len END;
  i := 0;
  WHILE i < t.len DO
    u := 0.0; v := 0.0;
    IF i < p.len THEN u := p.coeff[i] END;
    IF i < q.len THEN v := q.coeff[i] END;
    t.coeff[i] := u+v;
    i := i+1
  END;
  result := t
END Add;

With

L = max (p . len, q . len)

, the loop invariant is

0 \leq i \leq L

and, for

0 \leq k < i

, t.coeff[k] is the sum of the two extended input coefficients at

k

. The loop variant is

L - i

. The inputs remain unchanged throughout the loop, and at exit every active coefficient is correct. The time complexity is

O (L)

for the active arithmetic; assigning the fixed-capacity record can additionally copy its full capacity.

For the product, each pair of input terms contributes

a_{i} b_{j} x^{i + j}

. Initialize the active result to zero, then accumulate these pairwise contributions:

PROCEDURE Multiply(VAR p, q, result: Polynomial);
  VAR t: Polynomial; i, j, k: INTEGER;
BEGIN
  t.len := 0;
  IF (p.len > 0) & (q.len > 0) THEN
    t.len := p.len + q.len - 1
  END;
  (* Precondition: t.len <= Capacity. *)
  k := 0;
  WHILE k < t.len DO
    t.coeff[k] := 0.0; k := k+1
  END;
  IF t.len > 0 THEN
    i := 0;
    WHILE i < p.len DO
      j := 0;
      WHILE j < q.len DO
        t.coeff[i+j] := t.coeff[i+j]
                          + p.coeff[i]*q.coeff[j];
        j := j+1
      END;
      i := i+1
    END
  END;
  result := t
END Multiply;

The input representation invariants and the capacity precondition are assumed. No coefficient is accessed when either input is the zero polynomial. The initialization loop invariant says coefficients below

k

are zero; its loop variant is t.len-k.

For positive input lengths

m, n

, the outer loop invariant says that

0 \leq i \leq m

and each coefficient

t_{k}

equals

\sum_{0 \leq u < i} \sum_{0 \leq v < n u + v = k} a_{u} b_{v} .

The inner loop invariant adds the contributions with

u = i

and

0 \leq v < j

to that sum, while

0 \leq j \leq n

. The update adds exactly the next missing term at index

i + j

, preserving the inner loop invariant. The loop variants are

m - i

for the outer loop and

n - j

for the inner loop. On exit all pairs have contributed, yielding

(p + q)_{k} = a_{k} + b_{k}, (pq)_{k} = i + j = k \sum a_{i} b_{j} .

(2)

The product uses

O (mn + m + n)

arithmetic operations and a temporary coefficient array of capacity Capacity. Both operations allow trailing zeros; no extra normalization loop is required. Only the active coefficients are meaningful, so inactive record entries are never read by these operations. As in part (a), floating-point coefficients implement these formulas subject to rounding.

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

Use a doubly linked list, store both physical endpoints and its length, and maintain a flag for lazy reversal of a doubly linked list. This makes endpoint insertion and reversal constant time. Finding an arbitrary indexed element takes a traversal from whichever physical endpoint is nearer.

class LLBuffer extends ReversableBuffer {
  private class Node(val value: Int) {
    var prev: Node = null
    var next: Node = null
  }
  private var first: Node = null
  private var last: Node = null
  private var size = 0
  private var backwards = false

  // Methods from (ii) go here.
}

Define

F

to be the sequence of values obtained by starting at first and repeatedly following next until null. The representation invariant says that size is nonnegative; size == 0 holds exactly when both endpoints are null; otherwise there are exactly size distinct reachable linked list nodes, the final one is last, first.prev == null, last.next == null, and all neighboring links are reciprocal. These conditions make

F

finite and the physical linked list acyclic. The abstraction function is

s = {F reverse (F) if \neg ba c k w a r d s, if ba c k w a r d s .

The flag does not change the representation invariant. An empty physical linked list represents the empty sequence for either flag value. No client receives a linked list node reference, so clients cannot invalidate its links.

Figure 1.
Physical doubly linked list order and logical sequence order under lazy reversal of a doubly linked list
. **Details**.

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

Use a minimum stack: each linked list node caches the minimum of all values from that node down to the bottom. This handles duplicate minima without searching when one is removed.

class Stack {
  private class Node(val value: Int, val least: Int, val next: Node)
  private var top: Node = null

  def push(x: Int): Unit = {
    val m = if (top == null) x else math.min(x, top.least)
    top = new Node(x, m, top)
  }

  def pop(): Int = {
    require(!isEmpty)
    val x = top.value
    top = top.next
    x
  }

  def isEmpty: Boolean = top == null

  def min: Int = {
    require(!isEmpty)
    top.least
  }
}

The representation invariant is that the chain from top is finite and acyclic, and every reachable node q satisfies

q . l e a s t = {q . v a l u e min (q . v a l u e, q . n e x t . l e a s t) q . n e x t = n u ll, q . n e x t \neq = n u ll .

The abstraction function takes the values along this chain in top-to-bottom order. Thus pushing

x

changes

s

x : s

, and popping a nonempty

s

returns its head and leaves its tail. The cached-minimum equation follows for a new node from the previously valid chain; removing a head leaves every surviving equation unchanged. Consequently

p u s h, p o p, i s E m pt y, min each take O (1) worst-case time .

(2)

The bounds use the usual constant-cost allocation and integer arithmetic model. Storage is linear in the number of entries. min and pop require a nonempty stack; min leaves it unchanged.

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

Keep a running total in the mixin, and use only the inherited public operations. Updating after a successful superclass operation leaves the total unchanged if an empty pop fails its precondition.

trait SumPlugin extends Stack {
  private var total = 0

  override def push(x: Int): Unit = {
    super.push(x)
    total += x
  }

  override def pop(): Int = {
    val x = super.pop()
    total -= x
    x
  }

  def sum: Int = total
}

For this trait mixed directly into Stack, its representation invariant is

t o t a l = \sum s

, where

s

is the abstract stack sequence. A successful push adds exactly its argument and a successful pop removes exactly its returned value. Thus

s u m = the sum of the current stack entries, s u m (empty stack) = 0.

The mixin reads no private Stack fields. Its operations add constant time complexity. As in the paper's Int interface, an unbounded mathematical total requires excluding integer overflow, or replacing the accumulator with BigInt if the interface is allowed to change. A later mixin can transform a pushed value at a different point in the Scala trait linearization; the effect is analyzed in the next part.

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

The doubling mixin delegates with a transformed argument.

trait DoublePlugin extends Stack {
  override def push(x: Int): Unit = super.push(2 * x)
}

For A, the relevant Scala trait linearization is A, DoublePlugin, SumPlugin, Stack. A push first doubles the argument, then SumPlugin sees and sums that doubled value. The physical values are

2, 4, 6

and the total is

12

For B, the Scala trait linearization is B, SumPlugin, DoublePlugin, Stack. SumPlugin sums the original argument, while its super.push doubles the stored value. The physical values are still

2, 4, 6

, but the counter is

1 + 2 + 3 = 6

. Hence the two lines printed are

12
6

Equivalently,

a . s u m = 12, b . s u m = 6.

This is stackable trait modification: the order determines which arguments an outer mixin observes. In particular, the running-total specification from part (b) holds for A but does not survive the transforming inner mixin in B. With the given implementation, popping from B would subtract the doubled stored value, demonstrating why mixing individually sensible traits can break a combined representation invariant.

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

A simple current-value implementation works when

f

is a pure function, but sharing a mutable closure between copies would violate the independence requirement used in part (d). Use a memoized successor chain for stateful iterator copies: the generated sequence has shared cells, and each iterator has its own current-cell pointer.

object FunIter {
  final class Cell[T](val head: T, f: T => T) {
    lazy val tail: Cell[T] = new Cell[T](f(head), f)
  }
}

class FunIter[T](v: T, f: T => T) extends Iter[T] {
  private var cursor = new FunIter.Cell[T](v, f)

  def hasNext: Boolean = true

  def next(): T = {
    val x = cursor.head
    cursor = cursor.tail
    x
  }

  def copy(): Iter[T] = {
    val result = new FunIter[T](cursor.head, f)
    result.cursor = cursor
    result
  }
}

The representation invariant is that cursor points to the next cell to be returned, and each cell's lazy tail is computed at most once. The abstraction function is the infinite sequence of heads starting at that cell. Advancing changes only this iterator's pointer. A copy starts at the same cell, so both observe the same remaining heads even when their calls are interleaved:

n e x t returns v, f (v), f (f (v)), \dots; co p y preserves an independent position .

For a stateful

f

, the generator state must be privately owned by this shared chain; unrelated external calls to

f

must not change it. As usual, the values and transition must allow successive results to be observed without externally mutating old results. No interface can independently clone the hidden state of an arbitrary externally mutated closure from its function type alone. The chain avoids needing such cloning: a lagging copy reuses the already generated future instead of invoking

f

again.

Each new cell needs one transition and constant bookkeeping, but retained slower copies can keep a long generated prefix alive. This is an intentional space tradeoff that permits the stateful generator in part (d). No output is possible if computing a demanded transition itself fails or diverges.

Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Imperative programming / 8 / a / Solution 2026-10-31

Represent the set by a private list containing each value once. Normalize the constructor input as well as checking future insertions; otherwise duplicate initial entries would violate the intended set behavior.

class Set[T](contents: List[T]) {
  protected var elems: List[T] = contents.distinct

  def add(x: T): Unit = {
    if (!elems.contains(x)) elems = x :: elems
  }

  def delete(): T = {
    require(elems.nonEmpty)
    val x = elems.head
    elems = elems.tail
    x
  }
}

The representation invariant is that elems contains no duplicates under the chosen stable value equality; the abstraction function forgets its ordering and returns its set of elements. The protected field allows the subclass in part (d) to inspect its contents; that subclass is responsible for preserving the representation invariant if it mutates them.

Insertion makes the represented set

S \cup {x}

. Deletion requires

S \neq = \emptyset

, returns some

x \in S

, and leaves

S ∖ {x}

. Thus

a dd (x) : S^{'} = S \cup {x}; d e l e t e () : x \in S, S^{'} = S ∖ {x} .

Deletion does not promise to choose a minimum. With this linked list representation, insertion takes

O (∣ S ∣)

time complexity because of its membership check, while deletion takes

O (1)

. Values should not mutate in a way that changes their equality while stored.

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

An immutable object can widen its element type when adding a value by returning a new object. Introduce a lower type bound

U >: T

on the method's fresh type parameter.

class ISet[+T](contents: List[T]) {
  private val elems: List[T] = contents.distinct

  def add[U >: T](x: U): ISet[U] = {
    val widened: List[U] = elems
    if (widened.contains(x)) new ISet[U](widened)
    else new ISet[U](x :: widened)
  }

  def delete(): (T, ISet[T]) = {
    require(elems.nonEmpty)
    (elems.head, new ISet[T](elems.tail))
  }
}

As before, the representation invariant excludes duplicates, and the abstraction function returns the unordered set of entries. The constructor normalization makes the representation invariant hold even for repeated initial entries. Both operations construct a fresh set object and leave the original object unchanged, including when addition finds an existing member.

For a receiver representing

S

, the new object returned by add represents

S \cup {x}

. Deletion returns a pair

(x, R)

with

x \in S

and

R

representing

S ∖ {x}

. Crucially,

a dd [U >: T] (x : U) : I S e t [U], d e l e t e () : (T, I S e t [T]) .

The widened list is valid because immutable List itself has a covariant type parameter. A client can view an ISet[Int] as ISet[Any], but adding a string creates a separate widened result; it cannot put a string into the old integer set. This explains how using immutable objects makes the desired type variance sound. A direct add(x: T) on a covariant software class would still violate the variance-position rule; immutability alone does not repair an incorrectly typed method signature.

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

Use an upper type bound requiring each element type to implement the supplied comparison interface for its own type. This is F-bounded polymorphism.

trait Ordered[T] {
  def <(that: T): Boolean
}

class MinSet[T <: Ordered[T]](contents: List[T])
    extends Set[T](contents) {
  def min: T = {
    require(elems.nonEmpty)
    var best = elems.head
    var rest = elems.tail
    while (rest.nonEmpty) {
      if (rest.head < best) best = rest.head
      rest = rest.tail
    }
    best
  }
}

Use this locally defined Ordered, rather than silently substituting the standard library's different comparison interface. The type bound makes rest.head < best well typed. To interpret the result as a minimum, require the comparison to be a consistent strict total order; merely providing a method named < cannot establish its mathematical laws.

The loop invariant is that best is a minimum among the entries already inspected, and rest is exactly the uninspected suffix. Comparing its next head with best preserves that property. The loop variant is the length of rest. On termination,

min \in S, \forall x \in S, \neg (x < min) .

The method leaves the set unchanged, takes

O (∣ S ∣)

time complexity under constant-cost comparisons, and uses constant auxiliary space. It requires a nonempty set; inherited insertion and deletion continue to preserve the duplicate-free representation invariant.

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

Follow the next reference for the desired level, stopping at the tail. This returns the genuine nodes in their linked list order, excluding both sentinel nodes.

def nodesAt(level: Int): List[Node] = {
  require(0 <= level && level < NumLevels)
  val out = scala.collection.mutable.ListBuffer.empty[Node]
  var n = head.nexts(level)
  while (n ne tail) {
    out += n
    n = n.nexts(level)
  }
  out.toList
}

Write

L_{h}

for the resulting sequence of nodes at level

h

. The abstraction function is

α = map (datum, L_{0}) .

It preserves repetitions, because distinct nodes may carry equal values. A suitable representation invariant requires the following:

head and tail are distinct sentinel nodes with the specified extreme values; every node has a nexts array of length NumLevels.
For each level, following references from head gives a finite acyclic chain ending at tail, then null; the data along that chain are nondecreasing. Genuine values lie strictly between the sentinel values.
Each $L_{h + 1}$ is a subsequence of $L_{h}$ by node identity, so the relative order of equal-valued nodes agrees across levels. Every genuine node occurs in $L_{0}$ and on a contiguous initial collection of levels.
A genuine node absent from a level has null in that level's slot. Tail slots are all null; every other slot on a chain points to the next member of that chain.

These structural requirements make the traversal terminate and make descending through levels valid. A probabilistic height distribution is a performance policy, rather than a condition needed for the abstraction function to describe an ordered sequence.

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

Start at the highest level. Move right only while the next key is strictly smaller than x, then descend without returning to head.

def findPreds(x: Int): Array[Node] = {
  require(Int.MinValue < x && x < Int.MaxValue)
  val preds = new Array[Node](NumLevels)
  var n = head
  var level = NumLevels - 1
  while (level >= 0) {
    while (n.nexts(level).datum < x) {
      n = n.nexts(level)
    }
    preds(level) = n
    level -= 1
  }
  preds
}

At each inner loop head, n belongs to the current level and has key below x. Every node already passed has key below x. The representation invariant ensures that n also belongs to the next lower level. Stopping just before a key at least x therefore gives

preds (h) . datum < x \leq preds (h) . nexts (h) . datum .

The tail prevents a null dereference during the comparison. Strict comparison makes the predecessor lie before the first occurrence of x, including duplicates. On the source diagram, findPreds(14) yields data

[11, 9, 9, - \infty]

, in increasing level order.^[ref]

With the customary random-level policy this has expected logarithmic time complexity for a suitably sized level cap; an unlucky skip list can require a linear scan. No deterministic logarithmic guarantee is claimed.

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

Pick the new node's highest level once, and splice the same node into every level up to that height. pickLevel must return a value in 0 until NumLevels.

def add(x: Int): Unit = {
  require(Int.MinValue < x && x < Int.MaxValue)
  val preds = findPreds(x)
  val highest = pickLevel
  require(0 <= highest && highest < NumLevels)
  val n = new Node(x)
  for (level <- 0 to highest) {
    n.nexts(level) = preds(level).nexts(level)
    preds(level).nexts(level) = n
  }
}

The fresh array contains null above the chosen height. At each changed level the new node lies after a smaller value and before a value at least x. Every new occurrence is placed before all previous equal-valued nodes, consistently across levels. Therefore the representation invariant is preserved and

α_{new} = α_{old} with one extra occurrence of x .

The splice work is

O (highest + 1)

in addition to one skip list search.

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

The representation invariant is

N \geq 0

, rows.length == N, and every rows(i) is a nonnull finite list of entries

(j, x)

satisfying

0 \leq j < N, x \neq = 0.0, column indices strictly increase along each row .

Strict increase excludes repeated columns. The abstraction function gives

A_{ij} = x

when the unique entry

(j, x)

occurs in rows(i), and

A_{ij} = 0

otherwise. Thus omitted positions represent zero; omission does not mean an unknown matrix entry.

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

Select entries having the requested column. The representation invariant ensures that the selected list has length at most one.

def get(i: Int, j: Int): Double = {
  require(0 <= i && i < N && 0 <= j && j < N)
  val entries = rows(i).filter(e => e._1 == j)
  if (entries.isEmpty) 0.0 else entries.head._2
}

Consequently

get (i, j) = A_{ij} .

This version follows the hint and has time complexity linear in the number of stored entries in row i. An ordered early-exit scan is also possible.

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

Keep the entries before column j, discard any old entry at j, and retain those after it. Insert the replacement only when it is nonzero.

def set(i: Int, j: Int, x: Double): Unit = {
  require(0 <= i && i < N && 0 <= j && j < N)
  val before = rows(i).takeWhile(e => e._1 < j)
  val after = rows(i).dropWhile(e => e._1 <= j)
  val middle: Row = if (x == 0.0) Nil else List((j, x))
  rows(i) = before ::: middle ::: after
}

All indices in before are below j and all in after are above it, so the representation invariant is preserved. Other rows and all other column values remain unchanged:

A_{ij}^{'} = x, A_{k l}^{'} = A_{k l} when (k, l) \neq = (i, j) .

Assigning zero removes storage for that entry. The time complexity is linear in the stored row length.

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

Entry

(j, x)

in source row i becomes entry

(i, x)

in destination row j. Visit source rows in descending order and prepend, producing increasing destination column order without a sorting pass.

def transpose: SparseMatrix = {
  val out = new SparseMatrix(N)
  var i = N - 1
  while (i >= 0) {
    for ((j, x) <- rows(i)) {
      out.rows(j) = (i, x) :: out.rows(j)
    }
    i -= 1
  }
  out
}

Before processing source row i, each destination row contains exactly the contributions from source rows with index greater than i, in increasing index order. Prepending index i preserves that order, and each source position is unique. Hence the representation invariant holds and

out_{ji} = A_{ij}, O (N + M) time .

The source sparse matrix is unchanged.

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

A demand-driven filtering iterator needs one cached accepted value. Otherwise hasNext would either lose an element or consume another accepted value every time it is queried.

def filterIter[T](p: T => Boolean, it: Iter[T]): Iter[T] =
  new Iter[T] {
    private var buffered: Option[T] = None
    private var finished = false
    private def fill(): Unit = {
      while (buffered.isEmpty && !finished) {
        if (!it.hasNext) finished = true
        else {
          val x = it.next()
          if (p(x)) buffered = Some(x)
        }
      }
    }
    def hasNext: Boolean = {
      fill()
      buffered.nonEmpty
    }
    def next(): T = {
      fill()
      require(buffered.nonEmpty)
      val answer = buffered.get
      buffered = None
      answer
    }
  }

The representation invariant says that buffered holds at most one accepted value. The represented sequence is the buffered value, if present, followed by the subsequence of the underlying remainder satisfying the predicate. Filling moves the next accepted value into the cache and discards only rejected values, so this abstract sequence is unchanged by hasNext. Clearing the cache in next removes its head. Thus

α (filterIter (p, i t)) = filter (p, α (i t)) .

next works even when the client has not first called hasNext; exhaustion violates its stated precondition. As with ordinary iterator adapters, clients should give this wrapper exclusive consumption of it, and the predicate should give a stable answer for each element. One call may scan several rejected elements, but across a complete traversal each source element is consumed once. Cache storage is constant.

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Imperative programming / 7 / a / Solution 2026-10-31

Store characters in a mutable dynamic array. Its length is maintained by the collection, giving constant-time size.

class DocImpl extends Doc {
  private val text = scala.collection.mutable.ArrayBuffer.empty[Char]
  def insert(x: Char, pos: Int): Unit = {
    require(0 <= pos && pos <= text.length)
    text.insert(pos, x)
  }
  def delete(pos: Int): Char = {
    require(0 <= pos && pos < text.length)
    text.remove(pos)
  }
  def read(pos: Int): Char = {
    require(0 <= pos && pos < text.length)
    text(pos)
  }
  def size: Int = text.length
}

The representation invariant requires a nonnull private dynamic array containing a finite sequence of characters, with its internal collection invariant maintained by the library. The abstraction function is

α (text) = ⟨ text (0), \dots, text (length - 1)⟩ .

Insertion allows the end position and shifts the suffix right; deletion returns exactly the removed character and shifts the suffix left. read leaves the abstract state unchanged. size equals the abstract sequence length in

O (1)

time complexity. Indexed reads are also constant time; insertion and deletion may take linear time, which the question permits.

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

Keep 26 cached counts, updating them after a successful delegated edit. Count exactly lowercase letters; the query alphabet does not make uppercase letters the same character.

trait CharTrackPlugIn extends Doc {
  private val counts = Array.fill[Int](26)(0)
  private def lower(x: Char): Boolean = 'a' <= x && x <= 'z'
  abstract override def insert(x: Char, pos: Int): Unit = {
    super.insert(x, pos)
    if (lower(x)) counts(x - 'a') += 1
  }
  abstract override def delete(pos: Int): Char = {
    val x = super.delete(pos)
    if (lower(x)) counts(x - 'a') -= 1
    x
  }
  def getCount(x: Char): Int = {
    assert(lower(x))
    counts(x - 'a')
  }
}

For an initially empty underlying document that stores inserted arguments unchanged, the representation invariant is

counts (c - ’a’) = # {i : read (i) = c} (c = ’a’, \dots, ’z’) .

Insertion increments precisely the inserted lowercase character's count. Deletion uses the returned character, avoiding an extra indexed read and decrementing the character actually removed. Updating after super means a rejected edit leaves the counts unchanged. Both the added update work and getCount use

O (1)

time complexity and fixed storage.

The abstract override methods implement a stackable trait modification: they require a concrete document implementation further along the delegation chain. The invariant above depends on subsequent layers preserving inserted characters. Part (d) deliberately composes a transforming layer that can break this assumption; that is the transform-sensitive trait frequency counter phenomenon.

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

Store the minimal elements of the finite generating set. The represented upper set itself may be infinite; the code manipulates its finite basis.

class UpSet[T <: Ordered[T]](c: Set[T]) extends Ordered[UpSet[T]] {
  private val basis: Set[T] = minimal(c)
  def contains(x: T): Boolean = basis.exists(a => a <= x)
  def intersection(that: UpSet[T]): UpSet[T] = {
    val generators: Set[T] =
      for (a <- basis; b <- that.basis) yield a.lub(b)
    new UpSet[T](generators)
  }
  def <=(that: UpSet[T]): Boolean = basis.forall(a => that.contains(a))
  def lub(that: UpSet[T]): UpSet[T] =
    new UpSet[T](basis union that.basis)
}

The abstraction function and representation invariant are

α (B) =↑ B = {x : \exists b \in B, b \leq x}, B finite with no strictly comparable distinct values .

Removing nonminimal generators preserves the upward closure: in a finite generating set, repeatedly descending below any discarded element must reach a retained minimal element. Thus the constructor represents exactly the required finitely generated upper set.

Membership follows directly from the abstraction function. For intersection, an element

x

lies above some

a \in B

and some

b \in C

exactly when it lies above their least upper bound:

(a \leq x \land b \leq x) ⟺ a \lor b \leq x .

(2)

The forward implication is the defining leastness property; the reverse uses that

a \lor b

is an upper bound and transitivity. Consequently

↑ B \cap ↑ C =↑ {a \lor b : a \in B, b \in C} .

(3)

Recomputing minimal elements therefore yields a finite basis for the exact intersection.

For subset inclusion, it suffices that every generator of the left-hand upper set belongs to the right-hand upper set. Necessity holds because each generator belongs to its own closure by reflexivity. Sufficiency holds because the right-hand set is upward closed. Finally,

↑ B \subseteq↑ C ⟺ \forall b \in B, \exists c \in C, c \leq b, (↑ B) \lor (↑ C) =↑ (B \cup C) .

(4)

Thus lub computes union, which is the least upper bound under subset inclusion. The empty basis represents the empty set; all four methods handle it without a special case. As in part (a), two distinct Scala objects may denote the same abstract ordered value. Retaining several equivalent representatives is harmless: they generate the same upward closure, and the strict-comparison test removes only genuinely nonminimal values.