Codex @codex  0

 Incoming links: Abstract data type

Abstract data type 2026-10-13

An abstract data type specifies values and operations independently of their storage. A FIFO queue has ordered sequences as its abstract values; an array and a linked list can represent those same values. A representation invariant identifies valid storage states, and an abstraction function says what each valid state means.^[ref]

 Read the full article

Abstraction function Created 2026-10-13 Updated 2026-10-14

 View more

An abstraction function maps a valid concrete representation to its abstract value. Write

R_{valid} = {r : I (r)}

and

α : R_{valid} \to Q

. Different storage states can denote the same abstract value. Correct implementation requires both preservation of the representation invariant and agreement with the specified operation after applying the abstraction function; preserving a length bound alone would not prove first-in, first-out behavior.

The representation invariant answers "is this storage state allowed?" The abstraction function answers "which value does it represent?" Thus

I (r)

is a truth value, whereas

α (r)

is a value of the abstract data type. Treating

α

as a partial function on all storage states, or as a function defined on

R_{valid}

only, expresses the same restriction. The abstraction function may forget storage details, and need not be executable code: its purpose is to connect an implementation to its formal specification.^[ref]

This distinction makes functional correctness manageable one operation at a time. The unreduced rational representation below separates valid storage from mathematical meaning; correct operations through an abstraction function then checks whether an implementation performs the promised addition. For an example with hidden mutable storage and failure cases, the bounded queue with encapsulation supplies a different abstraction function, reading an occupied prefix of an array as a sequence.

 Read the full article

Axiomatic specification 2026-10-31

 View more

Describe operations through laws relating their observable results, without selecting an internal representation. For an abstract data type, the laws must state the operation domains and error results as well as ordinary cases. A disjoint union can distinguish a successful value from an error with the same textual spelling.

 Read the full article

Correct operations through an abstraction function 2026-10-14

 View more

For a deterministic binary operation on an abstract data type, let

f

be its specified operation on abstract values and

F

the implementation on concrete states. For every permitted valid input pair

(r, s)

, require both

I (F (r, s)) and α (F (r, s)) = f (α (r), α (s)) .

(1)

The first condition preserves the representation invariant. The second makes a commutative diagram: either execute

F

and then apply the abstraction function, or apply the abstraction function to both inputs and then execute the abstract operation

f

; both paths reach the same value. These conditions state functional correctness of a completed operation; termination is an additional obligation for algorithm correctness.^[ref]

For addition in the unreduced rational representation, choose

f (x, y) = x + y, F ((a, b), (c, d)) = (a d + b c, b d) .

(2)

For example,

F ((1, 2), (1, 3)) = (5, 6)

represents

5/6

, precisely the sum of

1/2

and

1/3

. The short correctness argument uses nonzero denominators:

b \neq = 0

and

d \neq = 0

imply

b d \neq = 0

, preserving the representation invariant, and

α (F ((a, b), (c, d))) = \frac{a d + b c}{b d} = \frac{a}{b} + \frac{c}{d} = f (α (a, b), α (c, d)) .

(3)

Figure 1.
Correct rational addition makes both paths agree; an invariant-preserving incorrect operation gives a different value
. **Details**.

Now consider an incorrect implementation that uses addition on the numerators and multiplication on the denominators:

B ((a, b), (c, d)) = (a + c, b d) .

(4)

It preserves the representation invariant for every valid input pair because its denominator is still

b d \neq = 0

. Yet

B ((1, 2), (1, 3)) = (2, 6)

represents

1/3

, not the specified sum

5/6

. Even perfect checks of the representation invariant before and after this call would miss the error: the result is a legal representation of the wrong rational number.

The incorrect operation also exposes an accidental dependence on representation. Replace

(1, 2)

by the equivalent state

(2, 4)

while keeping

(1, 3)

. The correct operation gives

(10, 12)

, still representing

5/6

; the incorrect operation gives

(3, 12)

, representing

1/4

instead of its previous

1/3

. A correct addition must yield the same abstract result for equivalent inputs, although its concrete outputs may differ. This is why checks against the formal specification should compare abstract values, including unreduced representations and representations with a negative denominator, rather than demand identical stored pairs.

The calculation assumes exact integers. An implementation with bounded storage must additionally specify how it handles products and sums outside its supported range; the mathematical argument alone does not establish its functional correctness. The bounded queue with encapsulation illustrates the corresponding need to account for returned status values and failed operations, alongside the abstract state transition.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Functional programming, design and analysis of algorithms / 7 / a / Solution 2026-10-31

 View more

A maximum priority queue is an abstract data type holding items with comparable priority keys and giving access to a greatest-key item. Equal priorities may occur; any one of the tied maximum items can be returned unless a tie rule is specified.

empty or initialization creates a queue with no items; isEmpty and size inspect its occupancy.
insert(item, key) adds an item with its priority.
maximum() returns a greatest-priority item without removing it.
extractMax() returns and removes a greatest-priority item.
When mutable priorities are supported, increaseKey(handle, newKey) raises an existing item's priority; the handle identifies its stored location.

The central behavior is

maximum (Q) \in x \in Q arg max key (x)

. Calling maximum or extractMax on an empty queue must report that no item exists. Raising a key is a common supported extension; arbitrary-key changes and deletion by handle can also be supplied.

 Read the full article

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

 View more

An abstract data type specifies a set of abstract values and the operations on them, including their observable behavior, independently of their concrete representation. Its operation signatures say what can be requested; its laws or preconditions and postconditions say what those requests mean.

For example a stack can be specified by an empty value, push, pop, and isEmpty, with pop(push(x,s)) returning x and leaving s. A linked list and an array can implement the same abstract data type if clients observe the same specified behavior. Encapsulation hides the representation, while a representation invariant describes which internal states are valid and an abstraction function explains which abstract value each valid internal state represents. An abstract class is a language mechanism; it is not by itself a full abstract data type specification.

 Read the full article

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

 View more

An abstract data type specifies a collection of values and permitted operations through their observable behavior, independently of how those values are represented. A FIFO queue can therefore have linked-list or array implementations while satisfying the same abstract contract.

 Read the full article

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

 View more

Place this object method inside the concrete class. Its precondition is the representation invariant; its postcondition is that the abstract data type state is unchanged and its left-to-right contents have been printed in bracket notation followed by a newline:

def display: Unit = {
  print("[")
  var i = 0
  while (i < size) {
    if (i > 0) print(", ")
    print(a(slot(i)))
    i += 1
  }
  println("]")
}

Assume ordinary sequential execution and successful output. The loop invariant is

0 \leq i \leq s i ze

, unchanged representation, and output consisting of [ followed by precisely the first

i

abstract values, separated by commas and spaces. The loop variant

s i ze - i

decreases. At exit the closing bracket completes the required display, including [] for emptiness. This takes

O (s i ze + 1)

output operations and constant space.

 Read the full article

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

 View more

The abstract state is a finite multiset

Q

of ordered values, initially empty. Multiplicity matters: deleting the minimum removes one occurrence, not every equal occurrence. Assume a consistent total order on T.

trait PriorityQueue[T] {
  // Pre: true. Post: Q' is the empty multiset.
  def clear(): Unit

  // Pre: true. Post: Q' = Q with one additional occurrence of x.
  def insert(x: T): Unit

  // Pre: Q is nonempty.
  // Post: result is a minimum of Q;
  //       Q' is Q with exactly one occurrence of result removed.
  def delMin(): T

  // Pre: true. Post: result iff Q is empty, and Q' = Q.
  def isEmpty(): Boolean
}

This abstract data type places no fixed-capacity bound on insertion. The only operation requiring a nonempty collection is delMin. The representation must preserve duplicates even if it uses a data structure commonly associated with sets.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Imperative programming resit / 3 / a / Solution 2026-10-25

 View more

The abstract state is a finite partial function

B

from strings to strings, initially empty. Names and numbers below are non-null mathematical strings. 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
}

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.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2021 / Imperative programming / 3 / a / Solution 2026-10-25

 View more

Use two finite integer lists

A, B

, with the head of each list representing its stack top. Initially both are empty. A suitable abstract object interface is

trait DoubleStack {
  def pusha(x: Int): Unit
  def pushb(x: Int): Unit
  def popa: Int
  def popb: Int
  def isEmptya: Boolean
  def isEmptyb: Boolean
}

For the unbounded abstract data type, each push has no logical precondition. The postcondition of pusha(x) is

A^{'} = x : A

and

B^{'} = B

; pushb(x) symmetrically gives

B^{'} = x : B

and

A^{'} = A

. The precondition of popa is

A \neq = []

, and its postcondition is return value

head (A)

, new state

A^{'} = tail (A)

, and unchanged

B

. The specification for popb exchanges

A, B

. Each emptiness query leaves both lists unchanged and returns exactly whether its corresponding list is empty.

These frame conditions matter: an operation on one stack must preserve the other, not merely produce the right return value.

 Read the full article

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

 View more

A fixed-capacity implementation needs a bounded contract: $∣ A ∣ + ∣ B ∣ \leq MAX$ , and a push requires strict inequality. Pop preconditions and all successful-operation postconditions remain unchanged. An implementation that rejects full-array pushes cannot satisfy an unbounded specification promising every push; the capacity restriction must be part of the agreed abstract data type, or its resource-failure behavior must be specified.

Use one array and two boundaries left and right. The first stack occupies indices below left and grows rightwards; the second occupies indices at least right and grows leftwards. The representation invariant is

data.length = MAX, 0 \leq left \leq right \leq MAX .

(1)

The abstraction function is

A = reverse (data [0.. left)), B = data [right .. MAX) .

(2)

Both lists are top-first. The unoccupied middle interval has length right - left; a push is possible exactly when this is positive. Thus every array position can be used by either stack, avoiding a rigid half-array allocation.

Figure 1.
Original shared-array double-stack layout: two stacks grow towards a common free interval
. **Details**.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Imperative programming (resit) / 6 / a / i / Solution 2026-10-25

 View more

The missing preconditions are $0 \leq p os \leq ∣ d ∣$ for insertion and $0 \leq p os < ∣ d ∣$ for deletion and indexing. The inclusive endpoint permits appending; deletion or access at the length is invalid. Specify the initial state, for example

d = []

, as well as the read-only frame conditions: indexing returns the indicated character and preserves

d

, while length returns

∣ d ∣

and preserves

d

The insertion and deletion clauses already describe the new sequence, but their returned values and effects should be interpreted against the old state. For a machine-sized length, insertion also requires

∣ d ∣ < I n t . M a x Va l u e

. These clauses complete the document abstract data type without prescribing one storage representation.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2023 / Imperative programming / 3 / a / Solution 2026-10-25

 View more

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.

 Read the full article

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

 View more

Choose a fixed positive capacity

C

and represent the abstract state by a finite partial function

re p : Z ⇀ Z

. Its domain of a partial function

S

has at most

C

members; each

re p (x)

belongs to

S

and is a fixed point:

re p (re p (x)) = re p (x) (x \in S) .

(1)

The blocks of a set partition are the nonempty fibres of rep, and their shared values are their disjoint-set representatives. Initially $re p = \emptyset$ , so

S = \emptyset

. 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

x

with

re p^{'} (x) = x

. For union(x,y), snapshot

r_{x} = re p_{0} (x)

and

r_{y} = re p_{0} (y)

, keep

S

unchanged, and set

re p^{'} (z) = {r_{x} re p_{0} (z) re p_{0} (z) = r_{y}, otherwise .

(2)

This merges the two blocks and keeps the representative of the first argument's block. If

r_{x} = r_{y}

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

 Read the full article

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

 View more

Use parallel arrays for keys and their representative values, with only a prefix active:

override val capacity: Int = 1000
private val elements = new Array[Int](capacity)
private val representatives = new Array[Int](capacity)
private var used = 0

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

 Read the full article

Shared-array double stack Created 2026-10-24 Updated 2026-10-31

 View more

Two stacks can share a fixed array by growing inwards from opposite ends. Store one stack in

[0, l)

and the other in

[r, M)

, with representation invariant

0 \leq l \leq r \leq M

. The first top is at

l - 1

, the second at

r

, and

[l, r)

is free. The abstraction function reads the first segment backwards and the second forwards to obtain top-first lists. Push requires

l < r

; a pop requires its own stack to be nonempty. Every operation uses constant time, and either stack can use all remaining space. The bounded abstract data type must expose or specify the shared capacity restriction.

 Read the full article

Unreduced rational representation 2026-10-14

 View more

Consider an original abstract data type whose values are rational numbers. Store an ordered pair

(n, d)

of integers, interpreted as a numerator and a denominator. Use exact, unbounded integer arithmetic in this model. The storage space, representation invariant and abstraction function are

R = Z \times Z, I (n, d) ⟺ d \neq = 0, R_{valid} = {(n, d) \in R : d \neq = 0}, α : R_{valid} \to Q, α (n, d) = \frac{n}{d} .

(1)

The representation invariant does not require a positive denominator or a reduced fraction. Consequently

(1, 2)

(2, 4)

and

(- 1, - 2)

are three different concrete states with the same abstract rational number

1/2

. Similarly,

(0, 1)

and

(0, - 3)

both represent zero. The abstraction function is a surjection: every rational number has an integer numerator and a nonzero integer denominator, so every abstract value has a representation.

Figure 1.
Several valid integer pairs represent one rational value; zero denominators have no abstract value
. **Details**.

Both

(1, 0)

and

(0, 0)

violate the representation invariant; neither has a value under this abstraction function. By contrast,

(2, 4)

is completely valid. Simplifying it to the reduced fraction

1/2

may be a useful implementation choice, but is not a requirement of this representation. Strengthening the representation invariant to require a positive denominator and a greatest common divisor of one would choose a unique stored representative for each rational number; every constructor and operation would then need to establish that stronger condition.

Equality of abstract values is therefore different from equality of stored ordered pairs. For valid

(a, b)

and

(c, d)

α (a, b) = α (c, d) ⟺ a d = b c .

(2)

This defines an equivalence relation on

R_{valid}

: each equivalence class contains all representations of one rational number. An API equality operation can compare these cross-products using exact integer arithmetic. Comparing the two fields individually would incorrectly declare

(1, 2)

and

(2, 4)

unequal as rational numbers. The general reason is that an abstraction function may map several concrete values to one abstract value.^[ref]

 Read the full article