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 2019 Imperative programming resit 5 b Solution by
Codex 0 2026-10-25
Use the row boundary and cache its sum. The restriction on the initial total makes the fixed The additional representation invariant is . It initially holds. For
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()
}
}Move, write for the boundary at entry. The loop invariant says that rows before are unchanged, rows from through equal , rows from onwards still equal , and remaining equals the sum of the current entries. The loop variant is . 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 have been printed correctly; its loop variant is . The inner loop invariant says that the current row's first cells have been emitted correctly; its loop variant is . The final labels loop has the same decreasing loop variant, and prints exactly the first 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 4 c Solution by
Codex 0 2026-10-25
Push the right child before the left child so that the LIFO stack exposes the left child first:Let be the sequence of labels in the preorder traversal of . If the abstract pending stack, top first, is , the loop invariant is that the output already printed, followed by , 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.
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)
}
}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 time and pending references for binary tree height .
Past exam of the year 1 of the computer science course of the University of Oxford 2019 Imperative programming resit 4 b Solution by
Codex 0 2026-10-25
Store the bottom of the stack at index zero and the top at the last occupied index:The representation invariant is that
class Stack {
private val MAX = 1000
private val data = new Array[Tree](MAX)
private var used = 0
// Pre: used < MAX.
def push(t: Tree): Unit = {
require(used < MAX, "Stack full")
data(used) = t
used += 1
}
// Pre: used > 0.
def pop: Tree = {
require(used > 0, "Stack empty")
used -= 1
val result = data(used)
data(used) = null
result
}
// Pre: true.
def isEmpty: Boolean = used == 0
}data.length==MAX, , and unused slots from used onwards contain null references. Occupied slots contain the stored Tree references; the stack itself need not forbid null values. The abstraction function, written with the first sequence element at the top, isInitially this is the empty sequence. push prepends its argument, pop removes and returns the first abstract element, and isEmpty reports whether the abstract sequence is empty. These postconditions follow directly from the index changes. Clearing a popped slot avoids retaining an otherwise unused tree reference. All three operations take time. No loops are needed. Past exam of the year 1 of the computer science course of the University of Oxford 2019 Imperative programming resit 4 a Solution by
Codex 0 2026-10-25
Treat a null reference as the empty binary tree and perform the visit before descending:By structural induction, the empty binary tree produces the empty output. A nonempty binary tree prints its root label, then the complete preorder traversal of the left subtree, then that of the right subtree. These are exactly the required output positions. The recursion terminates on a finite binary tree because each recursive call has strictly fewer vertices. For the three-node example, the output order is . The time complexity is linear in the number of vertices, with call stack depth bounded by the height of a binary tree plus a constant.
def preorderRecursive(t: Tree): Unit = {
if (t != null) {
println(t.datum)
preorderRecursive(t.left)
preorderRecursive(t.right)
}
} Past exam of the year 1 of the computer science course of the University of Oxford 2019 Imperative programming resit 3 g Solution by
Codex 0 2026-10-25
Use the move-to-front heuristic. Replace only 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.
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
} Past exam of the year 1 of the computer science course of the University of Oxford 2019 Imperative programming resit 3 f Solution by
Codex 0 2026-10-25
Let be the number of real contacts, and suppose the requested name is at position , counting from one. The implementation above makes exactly name-equality comparisons, including the successful comparison; null checks are not string comparisons. Thus the minimum is one, when the first real contact is requested, and the maximum is , when the last is requested. The precondition excludes unsuccessful recalls and recalls on an empty book. This counts calls to string equality, not individual character inspections within each call.
Past exam of the year 1 of the computer science course of the University of Oxford 2019 Imperative programming resit 3 e Solution by
Codex 0 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:The search loop invariant says that
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
}
}
}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 d Solution by
Codex 0 2026-10-25
Start with a private permanent header whose
next is null. Its two string fields are ignored. For a concrete state satisfying the representation invariant, define the abstraction functionThe representation invariant says that the header exists, the reachable real linked list is finite and acyclic, the header is not a real reachable linked list node, all real name/number fields are non-null strings, and real names are pairwise distinct. The real linked list nodes are owned by the book, so clients cannot mutate their fields through exposed references. Distinct names ensure that the displayed relation is a partial function. The initial empty linked list has abstraction . Reordering real linked list nodes changes the representation but not the abstract book. Past exam of the year 1 of the computer science course of the University of Oxford 2019 Imperative programming resit 3 c Solution by
Codex 0 2026-10-25
A permanent dummy header node gives even the first real linked list node a predecessor. Insertion into an empty linked list and deletion or movement of its first real linked list node then use the same link updates as internal cases. The header itself represents no contact, so it also removes the need to use a real name as a special end marker. A search still needs a null-end check.
Past exam of the year 1 of the computer science course of the University of Oxford 2019 Imperative programming resit 3 b Solution by
Codex 0 2026-10-25
The linked list node needs mutable fields for changing a stored number and rearranging links:The implementation will keep its real linked list nodes private to the
class Node(var name: String, var number: String, var next: Node)Book object and will not return linked list node references to clients. Past exam of the year 1 of the computer science course of the University of Oxford 2019 Imperative programming resit 3 a Solution by
Codex 0 2026-10-25
The abstract state is a finite partial function from strings to strings, initially empty. Names and numbers below are non-null mathematical strings. These preconditions and postconditions specify an abstract data type, independently of any linked list. In particular, a failed deletion leaves the abstract state unchanged, and recalling a missing name is outside the operation's specified domain.
store replaces an old binding if present; delete reports whether a binding existed.trait Book {
// Abstract state B: finite partial map String -> String; initially empty.
// Pre: name != null && number != null.
// Post: B' = B updated at name with number.
def store(name: String, number: String): Unit
// Pre: name != null && name is in dom(B).
// Post: result = B(name), and B' = B.
def recall(name: String): String
// Pre: name != null.
// Post: result iff name is in dom(B), and B' = B.
def isInBook(name: String): Boolean
// Pre: name != null.
// Post: result iff name was in dom(B); B' = B with name removed.
def delete(name: String): Boolean
} Past exam of the year 1 of the computer science course of the University of Oxford 2019 Imperative programming resit 2 c Solution by
Codex 0 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:The precondition is that every original entry lies in . The loop invariant istogether with: every active entry lies in , 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 .
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
}After array partitioning, the low subinterval has occurrences and possible values. If it is deficient, retaining it preserves the loop invariant. Otherwise , while the original active count is strictly less than ; subtraction givesThus 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 , 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 the loop is skipped and zero is returned. The Long value bounds avoid overflowing ; every internal pivot is at most , so its checked mathematical range fits Int.For the time complexity, let be the interval width and its active occurrence count before iteration . The loop invariant gives , and binary search gives . Each two-way array partition costs . Until the width reaches one, the widths are bounded by , so the total scan work is bounded by a geometric series plus loop overhead: overall, hence for positive . Partitioning the full array again at every iteration would instead lose this bound. Auxiliary space complexity is .
Past exam of the year 1 of the computer science course of the University of Oxford 2019 Imperative programming resit 2 a Solution by
Codex 0 2026-10-25
Let The loop invariant is , every entry of is less than , every entry of is at least , and the segment's multiset is unchanged. Entries outside are unchanged. When
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
}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 . At exit , so the returned has the required separation property, including empty segments and arbitrarily many duplicate entries. The time complexity is and auxiliary space complexity is . Past exam of the year 1 of the computer science course of the University of Oxford 2019 Imperative programming resit 1 e Solution by
Codex 0 2026-10-25
Print separators before all but the first term, so there is neither a leading nor a trailing plus sign:The loop invariant says that exactly the first unit fractions have been printed in order, separated by
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
}
} + , with no trailing separator. The loop variant is . The empty array is displayed as zero. Since and , the output is 5/7 = 1/2 + 1/5 + 1/70. The source's earlier example with middle denominator and final denominator contains the arithmetic typo; its final printing example is correct. Indeed , 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 1 d Solution by
Codex 0 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 The loop invariant is , , , , andWriting , the fraction for the extended prefix has numerator and denominator . These are the
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)
}nextN and nextD in the code. Reducing them preserves the value and restores coprimality. The loop variant is . At exit the helper returns the exact sum in lowest terms, including 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 is 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]Scala 2.12 BigInt API documentation. Checked representability with isValidInt before the potentially truncating toInt conversion
Past exam of the year 1 of the computer science course of the University of Oxford 2019 Imperative programming resit 1 c Solution by
Codex 0 2026-10-25
Maintain an accumulated array of denominators and an exact remaining fraction. The usual greedy algorithm can require a denominator larger than The loop invariant is , , all entries of
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 . 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
}e are positive, andAppending and replacing the residual by preserves this equality; division by the greatest common divisor preserves the residual's value. The loop variant is , by the proof in part (b). If nextN is zero, its greatest common divisor with nextD is nextD, giving residual . On normal exit the residual is zero and the returned array has exactly the required value. On the early-return branch, num copies of 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]Scala 2.12 BigInt API documentation. Methods gcd, isValidInt and toInt
. 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





