New articles - OurBigBook.com

Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Digital systems, linear algebra, introduction to formal proof (resit) / 3 / a / Solution by

Codex  0 2026-10-31

In the pictured single-cycle MIPS architecture, RegDst selects the write address of the register file: zero selects instruction bits

20 \dots 16

, the rt field used by a load; one selects bits

15 \dots 11

, the rd field used by an MIPS R-type instruction. RegWrite enables the clocked write to the selected processor register.

ALUSrc selects the second ALU input: zero uses the second register file read output, while one uses the sign-extended 16-bit immediate field. The zero signal is produced by the ALU, rather than being an opcode-decoder output: it is one exactly when the ALU result is zero. During beq, the ALU subtracts its operands, so zero tests equality. The diagram combines it with Branch to select the branch target instead of

PC + 4

TakeBranch = Branch \land zero .

Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Digital systems, linear algebra, introduction to formal proof (resit) / 2 / e / Solution by

Codex  0 2026-10-31

The custom CMOS circuit uses eight NMOS transistors and eight PMOS transistors in the output networks, plus eight transistors in the four input CMOS inverters:

N = 8 + 8 + 4 \cdot 2 = 24 transistors .

The complementary types give an actively driven output at either supply rail. An NMOS transistor provides a strong connection to ground; a PMOS transistor provides a strong connection to

V_{DD}

. An NMOS transistor used alone to pass a high level loses gate overdrive as the output rises, giving a threshold-degraded high level; the complementary problem affects a PMOS transistor passing a low level. Complementary networks avoid these degraded levels and, ideally, have no direct supply-to-ground conducting path for a stable input. Physical leakage and switching current remain, but a resistive load and its continuous static current are unnecessary.

Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Digital systems, linear algebra, introduction to formal proof (resit) / 2 / d / Solution by

Codex  0 2026-10-31

A more economical static CMOS design follows from factoring the condition for

z = 0

. The output is low exactly when both input pairs disagree:

\neg z = (a \oplus c) \land (b \oplus d) = (a \neg c \lor \neg a c) (b \neg d \lor \neg b d) .

Generate

\neg a, \neg b, \neg c, \neg d

with four CMOS inverters. Write

n (x)

p (x)

for an NMOS transistor or PMOS transistor whose gate receives

x

. In the following network expressions, a dash means a series connection and

∥

means a parallel connection.

Connect this eight-device pull-down network between

z

and ground:

[(n (a) - n (\neg c)) ∥ (n (\neg a) - n (c))] - [(n (b) - n (\neg d)) ∥ (n (\neg b) - n (d))] .

(2)

The first parallel module conducts exactly when

a \neq = c

and the second exactly when

b \neq = d

. Their series connection therefore conducts precisely when

z

should be zero.

By complementary CMOS network duality, connect this eight-device pull-up network between

V_{DD}

and

z

[(p (a) ∥ p (\neg c)) - (p (\neg a) ∥ p (c))] ∥ [(p (b) ∥ p (\neg d)) - (p (\neg b) ∥ p (d))] .

(3)

A PMOS transistor conducts when its gate is zero. Consequently the first upper branch conducts when

(\neg a \lor c) \land (a \lor \neg c)

, namely

a = c

; the second conducts when

b = d

. Their parallel connection gives the required logical disjunction. For every stable binary input, exactly one of the pull-up network and pull-down network conducts.

Figure 1.
Complementary CMOS networks: eight PMOS transistors above the output and eight NMOS transistors below it
. **Details**.

The figure labels each MOSFET channel by its gate signal; the four input CMOS inverters are additional to the devices drawn.

Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Digital systems, linear algebra, introduction to formal proof (resit) / 2 / c / Solution by

Codex  0 2026-10-31

The four CMOS inverters use

4 \cdot 2

transistors, the four two-input NAND gates use

4 \cdot 4

, and the four-input NAND gate uses

8

. Therefore this particular design uses

N = 8 + 16 + 8 = 32 transistors .

Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Digital systems, linear algebra, introduction to formal proof (resit) / 2 / b / Solution by

Codex  0 2026-10-31

Each parenthesized pair in the given Boolean function tests equality of two input bits:

(a \lor \neg c) \land (\neg a \lor c) = (a \land c) \lor (\neg a \land \neg c) .

This is logical equivalence, or the two-input XNOR gate function. Thus

z

is one whenever either input pair agrees. Generate the four complemented inputs with four inverters, and define the following NAND gate outputs:

u_{1} u_{3} = NAND (a, c), = NAND (b, d), u_{2} u_{4} = NAND (\neg a, \neg c), = NAND (\neg b, \neg d) .

(2)

Feed these four outputs into a single four-input NAND gate. De Morgan's laws give

z = NAND (u_{1}, u_{2}, u_{3}, u_{4}) = a c \lor \neg a \neg c \lor b d \lor \neg b \neg d .

(3)

Here juxtaposition denotes logical conjunction. The construction uses only inverters, two-input NAND gates and one four-input NAND gate, as required.

Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Digital systems, linear algebra, introduction to formal proof (resit) / 2 / a / Solution by

Codex  0 2026-10-31

For a CMOS inverter, connect one PMOS transistor from the positive supply

V_{DD}

to the output and one NMOS transistor from the output to ground; drive both gates with the input

x

. When

x = 0

, the PMOS transistor conducts and the NMOS transistor is off; when

x = 1

, the reverse holds. Thus the output is

\neg x

, using two transistors.

For a four-input NAND gate, use four NMOS transistors in series between the output and ground, with gates

a, b, c, d

. Use four PMOS transistors in parallel between

V_{DD}

and the output, with the same gate signals. The pull-down network conducts exactly when all four inputs are one; the pull-up network conducts whenever at least one input is zero. Hence

y = \neg (a \land b \land c \land d), N = 8 transistors .

As usual for static CMOS, tie the NMOS transistor bodies to ground and the PMOS transistor bodies to

V_{DD}

Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Digital systems, linear algebra, introduction to formal proof (resit) / 1 / e / Solution by

Codex  0 2026-10-31

A file descriptor table belongs to a process: its small nonnegative integer indices are file descriptors, and each occupied entry points to an open file description. It also holds descriptor-specific information, such as whether the descriptor closes on a successful program replacement. There is one logical file descriptor table per process in the traditional model; implementations can let processes explicitly share one.

The system-wide open file table, called the file pointer table here, contains open file descriptions. Each entry records an opening's access mode, current file offset, reference count and reference to an in-memory inode. Duplicated file descriptors, including inherited ones, can refer to the same open file description and therefore share its file offset. Independent opens of the same file normally create separate open file descriptions and separate offsets. There is one logical system-wide open file table, with many entries.

The system-wide in-memory inode table caches the inodes currently needed, including shared file metadata, locking and reference information. Its identity key must include the file system as well as the inode number when several volumes are mounted. There is one logical system-wide active inode table, distinct from the persistent inode table stored on each volume. These are logical organizations, not requirements for a single contiguous array in memory.

process descriptor \to open-file description \to active inode \to disk blocks .

Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Digital systems, linear algebra, introduction to formal proof (resit) / 1 / d / Solution by

Codex  0 2026-10-31

The hard link count in an inode duplicates information recoverable by counting directory entries that refer to its inode number. Keeping the count makes the last-name test fast: a hard link removal need not search every file-system directory. A file-system consistency checker can independently recount the references and compare the result with the stored value.

Likewise, a block allocation bitmap summarizes ownership information recoverable from allocated inodes, their file data blocks, their indirect block pointers, and reserved file system structures. This summary makes allocation efficient and supplies an independent consistency check against multiply allocated or lost blocks. Replicated superblock information is another possible form of data redundancy, helping recovery if one copy is damaged. These examples have distinct benefits: a cached count or allocation summary saves work, while an independent or replicated representation helps detect or repair corruption. Consistent updating is essential; redundancy alone does not make a file system crash-safe.

redundancy supports efficient lookup, consistency checking and recovery.

Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Digital systems, linear algebra, introduction to formal proof (resit) / 1 / c / Solution by

Codex  0 2026-10-31

Use a block allocation bitmap, one bit per allocatable disk block number, or a free-block list. Allocation removes a free block from the free representation; deallocation inserts it. Reserved file system structures, including the inode table and the free-space representation itself, must never be offered as free file data blocks. Free inodes can be tracked separately by an inode allocation bitmap.

A file data block becomes reusable when the file system has removed its ownership from the file. This happens, for example, when truncation discards that portion of the file, or when the file is finally destroyed. Destruction requires both removal of its last hard link and release of its last live reference: unlinking an open file must not reclaim blocks still needed through an open file description. A memory-mapped file, if supported, also requires its references to be accounted for. The indirect block pointers' own blocks are reclaimed when they are no longer needed.

There are two relevant notions of accessibility. Pathname-accessible files are those reached from the root through valid directory entries, subject to permissions; their allocated blocks are found through their inodes. Already-open files can additionally remain accessible through file descriptors even after their last names disappear. Allocated file system structures and blocks pinned by an operation must also be excluded from allocation. A block allocation bitmap must therefore describe actual allocation, rather than merely the blocks of currently named regular files.

One processor can still run several processes and be interrupted. Updating ownership and the free-space representation must therefore be serialized with respect to competing operations, for example through an appropriate kernel critical section. Persistence across a crash additionally requires file-system crash consistency, such as ordered updates or file-system journaling.

last name removed \neq \Rightarrow open-file blocks immediately free .

Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Digital systems, linear algebra, introduction to formal proof (resit) / 1 / b / Solution by

Codex  0 2026-10-31

The file-system namespace is rooted at the root file-system directory. Each directory entry associates a local name with an inode number. To resolve a pathname, start at the root for an absolute pathname, or at the process's current file-system directory for a relative pathname, and look up successive components in successive file-system directories. A file-system directory is itself a file with a special interpretation for its data.

The inode table stores file metadata and the information locating contents. The file-system directory structure supplies names and the connections used in pathname lookup. Thus the file is the object represented by its inode, whereas a file name is one entry referring to that object. Two hard links can give the same file two names, possibly in different file-system directories. Renaming a file need not move its contents or change its inode number; after unlinking an open file, a file can temporarily have no names and still be accessible through an existing file descriptor.

names locate inodes; inodes describe files and locate contents.

Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Digital systems, linear algebra, introduction to formal proof (resit) / 1 / a / Solution by

Codex  0 2026-10-31

In the traditional Unix file system model, a regular file consists of file metadata in an inode and an ordered sequence of bytes stored in file data blocks. The inode records the type, owner, permissions, length, timestamps and hard link count, together with the information locating its file data blocks. A small file can use direct file data block addresses; a larger file can additionally use indirect block pointers, whose blocks contain further addresses rather than user data. The final file data block need not be completely occupied.

An inode number identifies an entry in the inode table of this file system; it identifies the file, rather than a particular piece of its contents. A disk block number identifies a fixed-size storage region on the volume. Resolving an inode number first obtains the inode; following its direct or indirect block pointers then finds the required file data block. The two numbers belong to different address spaces, even though the inode table itself occupies disk blocks.

inode number: file identity; block number: storage location.

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Imperative programming / 8 / c / Solution by

Codex  0 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.

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Imperative programming / 8 / b / Solution by

Codex  0 2026-10-31

Keep precisely those elements with no strictly smaller element in the input. Express strictness using the partial order itself, avoiding reliance on Scala reference equality.

def minimal[T <: Ordered[T]](xs: Set[T]): Set[T] =
  xs.filter { x =>
    !xs.exists(y => (y <= x) && !(x <= y))
  }

In a partial order,

y < x

means

y \leq x

and

x \neq \leq y

. Therefore

minimal (X) = {x \in X : ∄ y \in X, y < x} .

The empty set produces the empty set. An incomparable pair is retained in full; a minimal element need not be a least element. At most

O (∣ X ∣^{2})

order comparisons are needed, and only the supplied F-bounded generic interface is required.

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Imperative programming / 8 / a / Solution by

Codex  0 2026-10-31

The interval containment order compares the lower endpoints in reverse and the upper endpoints in their ordinary order. The smallest containing integer interval uses the smaller lower endpoint and the larger upper endpoint.

class Interval(val l: Int, val u: Int) extends Ordered[Interval] {
  require(l <= u)
  def <=(that: Interval): Boolean = that.l <= l && u <= that.u
  def lub(that: Interval): Interval =
    new Interval(math.min(l, that.l), math.max(u, that.u))
}

Endpoint comparison immediately proves reflexivity, transitivity, and antisymmetry on interval values. If two separately allocated instances have the same endpoints, they denote the same abstract interval; object identity is not the mathematical equality used by this partial order.

The returned interval contains both operands. Every other containing interval has a lower endpoint at most both original lower endpoints and an upper endpoint at least both original upper endpoints, so it also contains the returned hull. Hence

[l, u] \lor [l^{'}, u^{'}] = [min (l, l^{'}), max (u, u^{'})] .

This least upper bound need not equal the ordinary union: the hull of

[1, 2]

and

[5, 6]

[1, 6]

, including the gap.

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Imperative programming / 7 / d / Solution by

Codex  0 2026-10-31

The rightmost trait intercepts insertion first. In A, capitalization runs before counting, so the counter receives uppercase A and does not increment the lowercase count. In B, counting receives lowercase a, delegates to capitalization, and then increments the original lowercase argument's counter. Both concrete documents store uppercase A.

The exact output is

0
1

d 1. getCount (’a’) = 0, d 2. getCount (’a’) = 1.

This illustrates an order-sensitive stackable trait modification. In the second composition the cached count describes intercepted insertion arguments, and no longer the actual lowercase characters in the stored document. For example, deleting its uppercase A would not decrement the lowercase counter. A counter required to track actual contents under arbitrary transforming mixins would need a stronger composition contract or would inspect the stored character after insertion; such a change would alter the intended behavior of this example.

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Imperative programming / 7 / c / Solution by

Codex  0 2026-10-31

Convert lowercase alphabet letters before passing them to the next implementation. Already uppercase letters and other characters pass through unchanged.

trait CapitalisePlugIn extends Doc {
  abstract override def insert(x: Char, pos: Int): Unit = {
    val y = if ('a' <= x && x <= 'z') ('A' + (x - 'a')).toChar else x
    super.insert(y, pos)
  }
}

The character conversion uses the paper's contiguous lowercase and uppercase Latin ranges. Thus

insert(’a’,pos) delegates as insert(’A’,pos) .

Deletion, reading, and size need no overrides.

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Imperative programming / 7 / b / Solution by

Codex  0 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 / 7 / a / Solution by

Codex  0 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 / 6 / b / Solution by

Codex  0 2026-10-31

In Scala trait linearization, the rightmost mixed-in trait takes priority. Merge inherited linearizations while retaining a shared ancestor only at its final position; super advances to the next implementation in the resulting chain. Ignoring predefined bases, the lookup orders are

Life1, Exercise, Work, Life
Life2, Dance, Exercise, Program, Study, Work, Fun, Life
Life3, Program, Study, Work, Dance, Fun, Exercise, Life

For example, Dance alone has order Dance, Fun, Exercise, Life. In Life2, the additional Program branch already contains Fun before Life; keeping that shared ancestry in its later position moves Fun after Work, while Dance still takes priority. Reversing the mixins yields the third chain above.

Each describe first delegates and then prints, so the lines appear in the reverse of the method lookup order. The exact output, including the two blank lines, is

I live.
I work.
I exercise.

I live.
I have fun.
I work.
I study.
I program.
I exercise.
I dance.

I live.
I exercise.
I have fun.
I dance.
I work.
I study.
I program.

Lookup follows the linearization; these prints occur while the calls return .

The super inside a trait therefore need not call that trait's isolated textual parent; the receiving object's full Scala trait linearization controls the next body.