Topics (384k) Articles (398k) Users (410) Discussions (242) Comments (383) Files (13k) New article
Past exam of the year 1 of the computer science course of the University of Oxford 2023 Imperative programming 5 c Solution by
Codex 0 2026-10-25
A sufficient representation invariant is:
The abstraction function isThe last two conditions ensure each representative is a genuine member of its own block and that the abstract function is idempotent function. Cells beyond
used are unconstrained and ignored. When used == 0, these conditions hold vacuously and the abstraction function yields the empty map. This is an explicit-key version of quick-find, rather than a parent-pointer disjoint-set forest. Past exam of the year 1 of the computer science course of the University of Oxford 2023 Imperative programming 5 b Solution by
Codex 0 2026-10-25
override val capacity: Int = 1000
private val elements = new Array[Int](capacity)
private val representatives = new Array[Int](capacity)
private var used = 0The chosen bound is an explicit implementation parameter of the abstract data type; another a-priori positive bound works identically. The initial map is empty because
used == 0. Zero-filled unused cells are not members of the map, so zero and negative keys remain valid integers. Use DisjointSets consistently as the trait name; the source's prose variation DisjointSubsets does not change the declared interface. Past exam of the year 1 of the computer science course of the University of Oxford 2023 Imperative programming 5 a Solution by
Codex 0 2026-10-25
Choose a fixed positive capacity and represent the abstract state by a finite partial function . Its domain of a partial function has at most members; each belongs to and is a fixed point:The blocks of a set partition are the nonempty fibres of
rep, and their shared values are their disjoint-set representatives. Initially , so . Representatives need not be the minimum members of their blocks.trait DisjointSets {
val capacity: Int
// State: rep is a finite idempotent map, |dom rep| <= capacity.
// Initially: rep is empty; capacity is fixed and positive.
// Pre: x is absent and |dom rep| < capacity.
// Post: add x -> x; leave every old mapping unchanged.
def makeSet(x: Int): Unit
// Pre: x belongs to dom rep.
// Post: state unchanged; return rep(x).
def find(x: Int): Int
// Pre: x and y belong to dom rep.
// Post: merge their blocks, retaining old rep(x).
def union(x: Int, y: Int): Unit
}Precisely,
makeSet(x) extends the domain of a partial function by with . For union(x,y), snapshot and , keep unchanged, and setThis merges the two blocks and keeps the representative of the first argument's block. If , it is an identity operation. This deterministic design choice satisfies disjoint set union without imposing minimum-element representatives. The capacity bound is explicit in the abstract data type so that the bounded implementation does not silently strengthen makeSet's precondition. Past exam of the year 1 of the computer science course of the University of Oxford 2023 Imperative programming 4 f Solution by
Codex 0 2026-10-25
Update an existing node, otherwise append one fresh node while preserving the cycle:
def store(name: String, number: String): Unit = {
val p = find(name)
if (p != null) p.number = number
else {
val fresh = new Node(name, number, null)
if (last == null) {
fresh.next = fresh
last = fresh
} else {
fresh.next = last.next
last.next = fresh
last = fresh
}
}
}For an existing name, changing only its number realizes replacement in the abstract partial function. On an empty book, the new node points to itself, establishing a singleton cycle. On a nonempty book, its successor becomes the old first node and the old last points to it; advancing
last leaves the first node unchanged and closes the enlarged cycle. Since a full search established absence, name uniqueness is preserved. Thus the postcondition is exactly the old book with this name mapped to the supplied number, and all other entries unchanged. A store takes running time for the name search and additional pointer work. Past exam of the year 1 of the computer science course of the University of Oxford 2023 Imperative programming 4 e Solution by
Codex 0 2026-10-25
Starting at
last.next, visit each node once and stop when the traversal would return to its start. This helper is private so that callers do not receive writable nodes from the representation.private def find(name: String): Node = {
if (last == null) return null
val first = last.next
var p = first
do {
if (p.name == name) return p
p = p.next
} while (p ne first)
null
}Null means no entry has that name. The test
p ne first compares object identity, not the equality of name or number fields. At each iteration all previously visited nodes failed the name test. The finite simple cycle guarantees that either a match is found or the traversal returns to first after exactly one turn. A singleton cycle is inspected exactly once. Stopping at null instead would fail to terminate on this representation. Past exam of the year 1 of the computer science course of the University of Oxford 2023 Imperative programming 4 d Solution by
Codex 0 2026-10-25
private var last: Node = nullNull represents the empty book. In a nonempty book,
last.next is the first node, and following next makes one finite simple cycle containing last. Names are unique around that cycle. This representation makes appending a new entry constant-time once a failed name search has established absence. The abstraction function collects every name/number pair on one complete turn of the cycle, rather than following pointers until null. Past exam of the year 1 of the computer science course of the University of Oxford 2023 Imperative programming 4 c Solution by
Codex 0 2026-10-25
Save the next pointer before redirecting it, then advance the two working heads. No node is allocated and the name/number fields are untouched.
def reverseBook(): Unit = {
var prev: Node = null
var cur = list
while (cur != null) {
val following = cur.next
cur.next = prev
prev = cur
cur = following
}
list = prev
}Let be the original sequence of node identities, not just their possibly equal field values. Write for the sequence currently headed by
prev and for that headed by cur. A suitable loop invariant for in-place linked-list reversal iswith both working lists finite, acyclic, disjoint, together containing exactly the original nodes, and with every name and number unchanged. Here ++ means concatenation. Initially and . One iteration takes from the front of and replaces by . Since , the equation is preserved. Saving following before changing cur.next retains access to .The loop variant is the length of , decreasing by one. At exit , so ; assigning the head establishes reversal. The empty and singleton cases work without a special branch. The abstraction function of the phone book ignores order, so it still maps every original name to its original number. All original node identities are reused, with running time and auxiliary space.
Past exam of the year 1 of the computer science course of the University of Oxford 2023 Imperative programming 4 b Solution by
Codex 0 2026-10-25
Inside
LinkedListBook, traverse without modifying the head or any node:def printBook(): Unit = {
var p = list
while (p != null) {
println(p.name + ":" + p.number)
p = p.next
}
}The loop invariant is that precisely the prefix before
p has been printed, once per node, in list order; p heads the remaining suffix. The null-terminated linked list invariant proves termination and prevents duplicate output through cycles. An empty list prints nothing. The abstraction function is unchanged, and the traversal takes node visits for entries. Past exam of the year 1 of the computer science course of the University of Oxford 2023 Imperative programming 4 a Solution by
Codex 0 2026-10-25
Let denote the non-null nodes reachable from the head. The representation invariant requires a finite acyclic null-terminated linked list and pairwise distinct names among its reachable nodes. Names and numbers retain the interface's string data type interpretation; no ordering of names is required.
The abstraction function is the finite partial functionName uniqueness makes this a function, rather than a relation assigning multiple numbers to one name. Initially
list == null, so and the abstract book is empty. Unreachable allocated nodes are outside this abstract state. Past exam of the year 1 of the computer science course of the University of Oxford 2023 Imperative programming 3 f Solution by
Codex 0 2026-10-25
For each table index , let be the set of non-null nodes reachable by following
next. A sufficient representation invariant is:- The array has exactly buckets, and every bucket heads a finite acyclic linked list.
- The sets are pairwise disjoint, so one physical node cannot belong to two buckets.
- Every reachable node has a valid user identity, lies in bucket
hash(node.user), and has both counters between zero andInt.MaxValue. - User identities are unique among all reachable nodes, not merely within a single chain.
The abstraction function maps these nodes to the total functions of part (a): if the unique node for exists, and are its fields; otherwise both are zero. A stored record with two zero counters is harmless and has the same observable meaning as an absent record. This intentionally permits multiple concrete representations of the same abstract program state.
Initially every bucket is null, so the representation invariant holds and the abstraction function yields all zeros. The successful-update branch preserves every structural condition; the insertion branch creates a fresh node with a previously absent identity in its correct bucket. Both branches realize exactly the incoming-increment postcondition, demonstrating correct operations through an abstraction function.
Past exam of the year 1 of the computer science course of the University of Oxford 2023 Imperative programming 3 e Solution by
Codex 0 2026-10-25
The following method belongs inside the source class and uses the helper from part (d). It preserves the existing outgoing count, and a newly encountered user starts with exactly one incoming and zero outgoing payments.
def recordIncoming(user: Int): Unit = {
require(1 <= user && user <= 99999999, "invalid user identity")
val bucket = hash(user)
val p = find(user, table(bucket))
if (p == null) {
table(bucket) = new PaymentsHash.Node(user, 1, 0, table(bucket))
} else {
require(p.countIn < Int.MaxValue, "incoming count is full")
p.countIn += 1
}
}On a hit, exactly one field is incremented after the overflow check. On a miss, inserting at the bucket head preserves all existing records and gives precisely the required change from implicit zero to one. The given hash function must return an index in consistently for a given user. Its actual formula is not needed by this method. The nested private node class is accessible to its companion class in Scala, so retaining the source's
PaymentsHash.Node visibility is valid.[ref]Scala 2.13 classes and objects specification. Modifiers: private members are accessible to the enclosing template and its companion
Past exam of the year 1 of the computer science course of the University of Oxford 2023 Imperative programming 3 d Solution by
Codex 0 2026-10-25
Inside the supplied
PaymentsHash class, scan until a matching node or the end of the chain. A null return means the user has no record in this bucket.private def find(user: Int, head: PaymentsHash.Node): PaymentsHash.Node = {
var p = head
while (p != null && p.user != user) p = p.next
p
}The loop invariant says that every node already passed has a different user identity and
p heads the unexamined suffix. Short-circuit evaluation of && prevents dereferencing null. The representation invariant supplies an acyclic finite chain, so each unsuccessful step shortens that suffix and proves algorithm termination. The code changes no node fields. Past exam of the year 1 of the computer science course of the University of Oxford 2023 Imperative programming 3 c Solution by
Codex 0 2026-10-25
With a directly indexed array, use two parallel count arrays, or one array of count records, at each user identity. Both queries and increments take running time, with no hash collision. However, reserving positions for each of two four-byte counters uses about million bytes, roughly MiB before object overhead, even when only a few users have payments. Index zero is unused and all valid positions initially contain zero.
With a linked list, store one node
(user, countIn, countOut, next) for each active user. A scan locates a record, returning zero counts if absent; an increment creates a missing record or updates its counter. Storage is for stored users, but a query or update can require running time. Nodes also carry pointer and allocation overhead and lack direct indexed access.With a hash table using separate chaining, compute a hash bucket from the user identity and store its record in that bucket's linked list. The same zero-default convention applies to a missing record. With buckets and a well-distributing hash function, the expected operation cost is in terms of the load factor of a hash table; worst-case cost remains under severe collisions. Storage is , but a permanently fixed cannot maintain constant expected cost as grows without bound. A good distribution and, where permitted, hash table resizing address that trade-off.
Past exam of the year 1 of the computer science course of the University of Oxford 2023 Imperative programming 3 b Solution by
Codex 0 2026-10-25
Every operation requires . The queries have postconditions “return ” and “return ” respectively, leaving both functions unchanged. An incoming increment additionally requires and hasThe outgoing increment analogously requires , increments only , and preserves . These frame conditions prevent an implementation from accidentally changing another user's count. Here a subscript zero denotes the old program state.
trait Payments {
// All methods require 1 <= user && user <= 99999999.
// Queries leave the abstract state unchanged.
def incoming(user: Int): Int
def outgoing(user: Int): Int
// Require the corresponding old count < Int.MaxValue.
// Increment only that user's named count by one.
def recordIncoming(user: Int): Unit
def recordOutgoing(user: Int): Unit
}The preconditions and postconditions are part of the formal specification; the trait's type signatures alone cannot express all of them. The implementation below uses checked
require calls for the relevant invalid operations. Past exam of the year 1 of the computer science course of the University of Oxford 2023 Imperative programming 3 a Solution by
Codex 0 2026-10-25
Use an abstract data type with two total count functions, , where and . counts incoming payments and outgoing payments. Initially for every valid user. A user without a stored record is therefore observable as two zero counts; no separate registration operation is necessary.
The explicit bound matches the source's
Int record fields. Increment operations require space in the relevant count, so no integer overflow is permitted. An unbounded mathematical counting abstract data type would instead require an arbitrary-precision representation or an explicit overflow policy. The large user domain does not require allocating a record for every user: a sparse map with a default value can realize these total functions. Past exam of the year 1 of the computer science course of the University of Oxford 2023 Imperative programming 2 e Solution by
Codex 0 2026-10-25
To preserve the actual printed function, including its handling of nonpositive exponents and wrapping
Int bases, use a tail-recursive accumulator with the same multiplication order:def anotherfuncRec(x: Int, n: Long): Double = {
require(x > 0)
@scala.annotation.tailrec
def loop(y: Int, i: Long, result: Double): Double = {
if (i <= 0) result
else {
val nextResult = if (i % 2 == 1) result * y else result
loop(y * y, i / 2, nextResult)
}
}
loop(x, n, 1.0)
}Each recursive call corresponds to one source iteration and carries exactly its next program state. Hence it reproduces the printed numerical behavior, rather than silently repairing it. For positive
n, both routines use steps; for nonpositive n, both take constant time. The recursive call is in tail position, so Scala's tail-call optimization avoids a growing call stack; the annotation asks the compiler to check that condition.If the intended exact power is required instead, change the base and accumulator parameters of this same recurrence to
BigInt and require n >= 0, as in part (d). Its mathematical loop invariant becomes a recursion invariant, with the same logarithmic number of multiplication steps. Past exam of the year 1 of the computer science course of the University of Oxford 2023 Imperative programming 2 d Solution by
Codex 0 2026-10-25
The algorithmic intention is exponentiation by squaring to compute for . With exact arithmetic, its loop invariant isInitially
result = 1, y = x, and i = n. For an even integer , squaring y and replacing i by preserves the product. For an odd integer , first multiply result by y; then . The nonnegative loop variant i decreases by halving whenever positive. At exit , so the loop invariant yields result = x^n. There are 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 iterations the remaining exponent is , and the Int base is the signed 32-bit representative of modulo . 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 bit-complexity bound. Merely making the accumulator a
Double does not widen the separate Int base variable. Past exam of the year 1 of the computer science course of the University of Oxford 2023 Imperative programming 2 c Solution by
Codex 0 2026-10-25
Under exact integer arithmetic, the intended result is , using the ceiling function. A sufficient loop invariant isInitially , and the final disjunction is true. If the guard holds, the old value is below . Incrementing
i and doubling y therefore preserves and makes the new lower bound true. At exit . If , positivity of forces ; otherwise . Both cases establish the claimed postcondition. Doubling eventually reaches or exceeds any fixed positive , 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 , it reaches , wraps to 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 . 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 , 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 b Solution by
Codex 0 2026-10-25
Validate the complete input before doing the addition. The arrays use most-significant-digit-first positional notation. The result has one extra leading position, which contains either zero or the final carry.
def binaryAddition(x: Array[Int], y: Array[Int]): Array[Int] = {
require(x != null && y != null, "arrays must not be null")
require(x.length == y.length, "lengths must match")
val n = x.length
var k = 0
while (k < n) {
require((x(k) == 0 || x(k) == 1) &&
(y(k) == 0 || y(k) == 1), "digits must be 0 or 1")
k += 1
}
val answer = new Array[Int](n + 1)
var carry = 0
var j = n - 1
while (j >= 0) {
val column = x(j) + y(j) + carry
answer(j + 1) = column % 2
carry = column / 2
j -= 1
}
answer(0) = carry
answer
}A failed
require throws IllegalArgumentException, covering mismatched lengths, invalid binary digits and null arrays. The largest column sum is three, so the carry always lies in . The binary-addition carry invariant says that the already processed input suffixes equal the written result suffix plus the carry shifted to the next column. After the final column, placing that carry at position zero proves the returned value is the sum. Neither input array is modified. Equal empty inputs are accepted as zero and return Array(0); the specification imposes no positive-length restriction. Running time and result storage are . Past exam of the year 1 of the computer science course of the University of Oxford 2023 Imperative programming 2 a Solution by
Codex 0 2026-10-25
Repeated integer division by two generates the binary digits from least significant to most significant. Reverse the accumulated characters once, and treat zero separately.
def binaryCon(n: Int): String = {
require(n >= 0, "n must be nonnegative")
if (n == 0) return "0"
var remaining = n
val digits = new StringBuilder
while (remaining > 0) {
digits.append(if (remaining % 2 == 0) '0' else '1')
remaining /= 2
}
digits.reverse.toString
}Zero produces
"0"; positive inputs produce a binary number without leading zeros. No library routine performs the number-to-base conversion. Appending to the builder and reversing once gives linear work in the number of binary digits and uses that much output storage. Pinned article: Introduction to the OurBigBook Project
Welcome to the OurBigBook Project! Our goal is to create the perfect publishing platform for STEM subjects, and get university-level students to write the best free STEM tutorials ever.
Everyone is welcome to create an account and play with the site: ourbigbook.com/go/register. We belive that students themselves can write amazing tutorials, but teachers are welcome too. You can write about anything you want, it doesn't have to be STEM or even educational. Silly test content is very welcome and you won't be penalized in any way. Just keep it legal!
Intro to OurBigBook
. Source. We have two killer features:
- topics: topics group articles by different users with the same title, e.g. here is the topic for the "Fundamental Theorem of Calculus" ourbigbook.com/go/topic/fundamental-theorem-of-calculusArticles of different users are sorted by upvote within each article page. This feature is a bit like:
- a Wikipedia where each user can have their own version of each article
- a Q&A website like Stack Overflow, where multiple people can give their views on a given topic, and the best ones are sorted by upvote. Except you don't need to wait for someone to ask first, and any topic goes, no matter how narrow or broad
This feature makes it possible for readers to find better explanations of any topic created by other writers. And it allows writers to create an explanation in a place that readers might actually find it.Figure 1. Screenshot of the "Derivative" topic page. View it live at: ourbigbook.com/go/topic/derivativeVideo 2. OurBigBook Web topics demo. Source. - local editing: you can store all your personal knowledge base content locally in a plaintext markup format that can be edited locally and published either:This way you can be sure that even if OurBigBook.com were to go down one day (which we have no plans to do as it is quite cheap to host!), your content will still be perfectly readable as a static site.
- to OurBigBook.com to get awesome multi-user features like topics and likes
- as HTML files to a static website, which you can host yourself for free on many external providers like GitHub Pages, and remain in full control
Figure 2. You can publish local OurBigBook lightweight markup files to either OurBigBook.com or as a static website.Figure 3. Visual Studio Code extension installation.Figure 5. . You can also edit articles on the Web editor without installing anything locally. Video 3. Edit locally and publish demo. Source. This shows editing OurBigBook Markup and publishing it using the Visual Studio Code extension. - Infinitely deep tables of contents:
All our software is open source and hosted at: github.com/ourbigbook/ourbigbook
Further documentation can be found at: docs.ourbigbook.com
Feel free to reach our to us for any help or suggestions: docs.ourbigbook.com/#contact






