Past exam of the year 1 of the computer science course of the University of Oxford / 2023 / Imperative programming / 3

Use an abstract data type with two total count functions,

I, O : U \to {0, \dots, M}

, where

U = {1, \dots, 99999999}

and

M = 2^{31} - 1

I (u)

counts incoming payments and

O (u)

outgoing payments. Initially $I (u) = O (u) = 0$ 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

M

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.

b

 0  0

Solution

 0  0

Every operation requires

u \in U

. The queries have postconditions “return

I_{0} (u)

” and “return

O_{0} (u)

” respectively, leaving both functions unchanged. An incoming increment additionally requires

I_{0} (u) < M

and has

I^{'} (v) = {I_{0} (u) + 1 I_{0} (v) v = u, v \neq = u, O^{'} = O_{0} .

(1)

The outgoing increment analogously requires

O_{0} (u) < M

, increments only

O (u)

, and preserves

I

. 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.

c

 0  0

Solution

 0  0

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

O (1)

running time, with no hash collision. However, reserving

1 0^{8}

positions for each of two four-byte counters uses about

800

million bytes, roughly

763

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

O (K)

for

K

stored users, but a query or update can require

O (K)

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

B

buckets and a well-distributing hash function, the expected operation cost is

O (1 + K / B)

in terms of the load factor of a hash table; worst-case cost remains

O (K)

under severe collisions. Storage is

O (B + K)

, but a permanently fixed

B = 100

cannot maintain constant expected cost as

K

grows without bound. A good distribution and, where permitted, hash table resizing address that trade-off.

d

 0  0

Solution

 0  0

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.

e

 0  0

Solution

 0  0

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

[0, N)

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]

f

 0  0

Solution

 0  0

For each table index

b

, let

C_{b} = L (t ab l e (b))

be the set of non-null nodes reachable by following next. A sufficient representation invariant is:

The array has exactly $N > 0$ buckets, and every bucket heads a finite acyclic linked list.
The sets $C_{b}$ 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 and Int.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

u

exists,

I (u)

and

O (u)

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

a

Solution

b

Solution

c

Solution

d

Solution

e

Solution

f

Solution

 Ancestors (10)

 Discussion (0)

 Articles by others on the same topic (0)

Past exam of the year 1 of the computer science course of the University of Oxford / 2023 / Imperative programming / 3

 Discussion (0)  Subscribe (1)

 Discussion (0)