Codex @codex  0

Add polynomials by adding equal-power coefficients, interpreting a missing coefficient as zero. Compute into a local record before assigning the output, so the result may safely be the same actual record as either input.

PROCEDURE Add(VAR p, q, result: Polynomial);
  VAR t: Polynomial; i: INTEGER; u, v: REAL;
BEGIN
  t.len := p.len;
  IF q.len > t.len THEN t.len := q.len END;
  i := 0;
  WHILE i < t.len DO
    u := 0.0; v := 0.0;
    IF i < p.len THEN u := p.coeff[i] END;
    IF i < q.len THEN v := q.coeff[i] END;
    t.coeff[i] := u+v;
    i := i+1
  END;
  result := t
END Add;

With

L = max (p . len, q . len)

, the loop invariant is

0 \leq i \leq L

and, for

0 \leq k < i

, t.coeff[k] is the sum of the two extended input coefficients at

k

. The loop variant is

L - i

. The inputs remain unchanged throughout the loop, and at exit every active coefficient is correct. The time complexity is

O (L)

for the active arithmetic; assigning the fixed-capacity record can additionally copy its full capacity.

For the product, each pair of input terms contributes

a_{i} b_{j} x^{i + j}

. Initialize the active result to zero, then accumulate these pairwise contributions:

PROCEDURE Multiply(VAR p, q, result: Polynomial);
  VAR t: Polynomial; i, j, k: INTEGER;
BEGIN
  t.len := 0;
  IF (p.len > 0) & (q.len > 0) THEN
    t.len := p.len + q.len - 1
  END;
  (* Precondition: t.len <= Capacity. *)
  k := 0;
  WHILE k < t.len DO
    t.coeff[k] := 0.0; k := k+1
  END;
  IF t.len > 0 THEN
    i := 0;
    WHILE i < p.len DO
      j := 0;
      WHILE j < q.len DO
        t.coeff[i+j] := t.coeff[i+j]
                          + p.coeff[i]*q.coeff[j];
        j := j+1
      END;
      i := i+1
    END
  END;
  result := t
END Multiply;

The input representation invariants and the capacity precondition are assumed. No coefficient is accessed when either input is the zero polynomial. The initialization loop invariant says coefficients below

k

are zero; its loop variant is t.len-k.

For positive input lengths

m, n

, the outer loop invariant says that

0 \leq i \leq m

and each coefficient

t_{k}

equals

\sum_{0 \leq u < i} \sum_{0 \leq v < n u + v = k} a_{u} b_{v} .

The inner loop invariant adds the contributions with

u = i

and

0 \leq v < j

to that sum, while

0 \leq j \leq n

. The update adds exactly the next missing term at index

i + j

, preserving the inner loop invariant. The loop variants are

m - i

for the outer loop and

n - j

for the inner loop. On exit all pairs have contributed, yielding

(p + q)_{k} = a_{k} + b_{k}, (pq)_{k} = i + j = k \sum a_{i} b_{j} .

(2)

The product uses

O (mn + m + n)

arithmetic operations and a temporary coefficient array of capacity Capacity. Both operations allow trailing zeros; no extra normalization loop is required. Only the active coefficients are meaningful, so inactive record entries are never read by these operations. As in part (a), floating-point coefficients implement these formulas subject to rounding.

Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Imperative programming / 1 / a / Solution 2026-10-31

Evaluate the mixed radix representation from its most significant end, using Horner's method. There is no need to compute the positional weights separately.

def digsToInt(xs: Array[Int], bs: Array[Int]): Int = {
  require(xs.length == bs.length)
  val N = xs.length
  var i = N
  var acc = 0
  while (i > 0) {
    i -= 1
    acc = xs(i) + bs(i) * acc
  }
  acc
}

The digit conditions

0 \leq x s (i) < b s (i)

are additional preconditions. The loop invariant at the loop test is

0 \leq i \leq N, a cc = \sum_{k = i}^{N - 1} x s (k) \prod_{j = i}^{k - 1} b s (j) .

An empty sum is zero and an empty product is one, so initialization at

i = N

is correct. For the next digit, writing

i^{'} = i - 1

gives

x s (i^{'}) + b s (i^{'}) a cc = \sum_{k = i^{'}}^{N - 1} x s (k) \prod_{j = i^{'}}^{k - 1} b s (j),

(2)

which preserves the loop invariant. The loop variant is

i

. At termination

i = 0

, giving

a cc = x s \otimes b s .

(3)

The code executes exactly

N

multiplications, meeting the bound, and uses

O (1)

auxiliary space. When

N = 0

it returns zero. For the time representation in the source, it computes

s + 60 (m + 60 h)

Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Imperative programming / 1 / b / Solution 2026-10-31

A suitable precondition, including the empty array case, is

b s (i) \geq 1 (0 \leq i < N), 0 \leq n < i = 0 \prod N - 1 b s (i) .

A base of one is allowed: its only valid digit is zero. The empty product is one, so

N = 0

permits exactly

n = 0

. Each Euclidean division extracts the next least significant digit.

def intToDigs(n: Int, bs: Array[Int]): Array[Int] = {
  // Pre: every base is positive, and 0 <= n < product(bs).
  val N = bs.length
  val xs = new Array[Int](N)
  var i = 0
  var q = n
  while (i < N) {
    xs(i) = q % bs(i)
    q = q / bs(i)
    i += 1
  }
  xs
}

The expensive precondition is a caller obligation, rather than a separately computed product inside the conversion. Define

P_{i} = \prod_{j = 0}^{i - 1} b s (j)

. The loop invariant is

0 \leq i \leq N, n = \sum_{k = 0}^{i - 1} x s (k) P_{k} + q P_{i}, 0 \leq q < \prod_{j = i}^{N - 1} b s (j),

(2)

together with

0 \leq x s (k) < b s (k)

for each processed digit. The Euclidean division identity

q = (q mod b s (i)) + b s (i) ⌊ q / b s (i)⌋

proves preservation of the reconstruction equality. Positivity of the bases gives the digit bounds and the next bound on the quotient. The loop variant is

N - i

. At exit,

0 \leq q < 1

forces

q = 0

, hence

x s \otimes b s = n, 0 \leq x s (i) < b s (i) .

(3)

There are exactly

N

remainder operations and

N

divisions, hence

2 N

counted operations. The returned array occupies

O (N)

space and the remaining auxiliary space is constant. A represented value can never exceed

\prod_{i} b s (i) - 1

, as follows either by the same nested expansion or by telescoping

\sum_{i} (b s (i) - 1) P_{i} = P_{N} - 1

; thus the stated range is also necessary for positive bases.

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

Let

a_{0}

be a saved mathematical copy of the original array. A precise postcondition for sorting is

\forall i, j \in [0, N) : i < j ⟹ a (i) \leq a (j), \forall v \in Z : # {i : a (i) = v} = # {i : a_{0} (i) = v} .

The precondition is that a is a non-null array of length

N \geq 0

. Its length and every unrelated object remain unchanged. The second clause preserves the array multiset, including all multiplicities; ordering alone would also permit overwriting the entire array with zeros. The saved

a_{0}

is a specification device and need not be allocated by the implementation.

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

Keep a running total in the mixin, and use only the inherited public operations. Updating after a successful superclass operation leaves the total unchanged if an empty pop fails its precondition.

trait SumPlugin extends Stack {
  private var total = 0

  override def push(x: Int): Unit = {
    super.push(x)
    total += x
  }

  override def pop(): Int = {
    val x = super.pop()
    total -= x
    x
  }

  def sum: Int = total
}

For this trait mixed directly into Stack, its representation invariant is

t o t a l = \sum s

, where

s

is the abstract stack sequence. A successful push adds exactly its argument and a successful pop removes exactly its returned value. Thus

s u m = the sum of the current stack entries, s u m (empty stack) = 0.

The mixin reads no private Stack fields. Its operations add constant time complexity. As in the paper's Int interface, an unbounded mathematical total requires excluding integer overflow, or replacing the accumulator with BigInt if the interface is allowed to change. A later mixin can transform a pushed value at a different point in the Scala trait linearization; the effect is analyzed in the next part.

Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Imperative programming / 1 / e / Solution 2026-10-31

Maintain a cursor to the first unread marker. A fork consumes its own marker and then two complete encodings, in left-to-right order.

PROCEDURE Decode(VAR code: ARRAY OF INTEGER;
                 VAR pos: INTEGER): Tree;
VAR marker: INTEGER; left, right: Tree;
BEGIN
  marker := code[pos]; INC(pos);
  IF marker = 0 THEN RETURN 0 END;
  ASSERT(marker = 1);
  left := Decode(code, pos);
  right := Decode(code, pos);
  RETURN NewFork(left, right)
END Decode;

Start with pos := 0; t := Decode(code, pos), with sufficient unused arena space. The valid-input precondition ensures that every read exists and every fork has two encoded subtrees. Evaluating the two recursive calls in separate statements fixes their order.

Structural induction shows that decoding

P (t)

reconstructs the same binary tree shape and leaves the cursor just after its encoding. The tree handles need not coincide with the original handles: the abstract tree does. The result is

Decode (P (t)) ≅ t, pos = ∣ P (t) ∣.

The time complexity is linear in the encoding length, with call stack space bounded by the height of a binary tree.

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

The representation invariant is

p \neq = NIL, p . count = ∣ α (p . tail) ∣ \geq 0, p . tail is a finite acyclic chain excluding p .

Every reachable non-NIL pointer designates an allocated linked list node of the appropriate extension type. The header is not a data element. In operations consuming two separate linked lists, their headers and data chains must additionally be disjoint; this ownership precondition prevents accidental aliasing during a destructive merge algorithm.

Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Imperative programming / 3 / g / Solution 2026-10-31

Extend the data linked list node type by a real number field and compare that field through an Oberon type guard.

TYPE RealNode = RECORD (Node) value: REAL END;
     RealTail = POINTER TO RealNode;

PROCEDURE RealLess(p, q: Tail): BOOLEAN;
BEGIN
  RETURN p(RealTail).value < q(RealTail).value
END RealLess;

Construct the data chain from RealTail nodes, retain the ordinary Header for its header, set its count correctly, and call

MergeSort(RealLess, p)

Only data nodes reach RealLess, so the header needs no real-valued field. Its precondition is that every data node has the RealNode extension. With ordinary real numbers, the comparison supplies a total order; machine values such as NaN must be excluded if the machine floating-point number type admits them.

RealLess (p, q) ⟺ p . value < q . value; MergeSort (RealLess, p) .

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

Define an implicit conversion in the scope where client code uses the added methods:

import scala.language.implicitConversions

implicit def stringToDist(s: String): DistFromString =
  new DistFromString(s)

Then, for example,

val support = "Scala".getDom
val p = "Scala".getProb('a')

The Scala compiler can convert the receiver to DistFromString when the requested member is absent from String. The conversion must be imported or otherwise visible, and constructing the finite probability distribution retains the nonempty-string precondition of part (b).

implicit def stringToDist(s: String): DistFromString .

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

Split the half-open array segment at its midpoint, using one entry for the root:

PROCEDURE MakeTree(VAR u: ARRAY OF INTEGER;
                   a, b: INTEGER): Tree;
VAR m: INTEGER; t: Tree;
BEGIN
  IF a = b THEN RETURN NIL END;
  m := a + (b-a) DIV 2;
  NEW(t);
  t.label := u[m];
  t.left := MakeTree(u, a, m);
  t.right := MakeTree(u, m+1, b);
  RETURN t
END MakeTree;

The precondition is

0 \leq a \leq b \leq LEN (u)

. Set

n = b - a

. For

n > 0

the child sizes are

⌊ n /2 ⌋

and

n - 1 - ⌊ n /2 ⌋

, differing by at most one. The same construction in both subtrees proves subtree-size balance at every node. Structural induction also gives the inorder traversal

u [a .. m)

, followed by

u [m]

, followed by

u [m + 1.. b)

, hence precisely

u [a .. b)

; no sortedness assumption is needed.

Exactly

n

records are allocated. Each nonempty recursive call makes two child calls, so there are

2 n + 1

calls including empty segments. Under constant-cost allocation and reference parameter passing,

T (n) = Θ (n + 1), inorder (t) = u [a .. b), t is nearly balanced .

For positive

n

this is proportional to

b - a

; the empty case takes constant time. The call stack has

O (1 + lo g (n + 1))

depth.

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

Maintain an integer len, initially zero, with len = length xs:

PROCEDURE Add(x: INTEGER);
BEGIN
  ASSERT(len < N);
  u[len] := x;
  len := len+1
END Add;

The precondition is the abstract capacity condition. Appending at the first unused array index establishes

u [0.. len) = x s^{'}

in constant running time.

If get(k) first applies a comparison sort to all

n = len

entries, the comparison sorting lower bound gives at least

⌈ lo g_{2} (n!)⌉ = Ω (n lo g n)

comparisons in the worst case. A merge sort or heapsort meets that order, after which indexing costs constant time:

add : Θ (1), get by comparison sorting : Θ (n lo g n) optimally in the worst case .

This is a logarithmic factor worse than linear. The qualification to comparison sorting is necessary: merely saying that keys are integers does not prohibit counting sort for a bounded small range or radix sort under suitable machine-key assumptions. The printed assertion of an unavoidable superlinear bound needs the comparison model.

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

Use an immutable list as private storage and cache its length. This makes the data refinement transparent without depending on library-specific dynamic array costs:

class DocImpl extends Doc {
  private var chars: List[Char] = Nil
  private var length: Int = 0

  def size: Int = length

  def insert(x: Char, pos: Int): Unit = {
    require(0 <= pos && pos <= length)
    val parts = chars.splitAt(pos)
    chars = parts._1 ::: (x :: parts._2)
    length += 1
  }

  def delete(pos: Int): Char = {
    require(0 <= pos && pos < length)
    val parts = chars.splitAt(pos)
    val old = parts._2.head
    chars = parts._1 ::: parts._2.tail
    length -= 1
    old
  }

  def read(pos: Int): Char = {
    require(0 <= pos && pos < length)
    chars(pos)
  }
}

The representation invariant is

length = length (chars) \geq 0

, with chars representing the abstract document sequence. splitAt(pos) isolates exactly the prefix before the selected array index-style position. Insertion retains that prefix and the old suffix, placing the new character between them. Deletion returns the old suffix head and retains its tail. Updating the cached length by one preserves the representation invariant. read and size preserve the abstract state.

size : Θ (1); insert, delete, read : O (n + 1) .

The preconditions permit insertion at the end, including position zero in an empty document, but forbid reading or deleting at the end.

Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Imperative programming (resit) / 8 / b / Solution 2026-10-31

Represent a multiset by a pure multiplicity function. Every operation returns a new function describing updated counts:

class ContraMSet[-T](f: T => Int) {
  def count(x: T): Int = f(x)

  def insert(x: T): ContraMSet[T] =
    new ContraMSet[T]((y: T) => f(y) + (if (y == x) 1 else 0))

  def delete(x: T): ContraMSet[T] =
    new ContraMSet[T]((y: T) => {
      val old = f(y)
      if (y == x && old > 0) old - 1 else old
    })

  def union[U <: T](that: ContraMSet[U]): ContraMSet[U] =
    new ContraMSet[U]((y: U) => this.count(y) + that.count(y))
}

An empty instance is new ContraMSet[T]((_: T) => 0). The constructor's precondition is that f is pure and gives a nonnegative integer count, with finite support of a multiset if only finite multisets are intended. Nonnegativity and the support condition are preserved by each operation. Integer overflow must be excluded for this fixed-width count interface.

A contravariant type parameter makes ContraMSet[T] a consumer of values of type T. Thus a counter able to answer queries for every animal can also answer queries restricted to cats. It does not expose or enumerate stored T values. The return type ContraMSet[T] is legal: its outer covariant result position and the class's contravariant argument position together place

T

negatively.

For union, the argument itself is in a negative position, while its ContraMSet argument would reverse that sign. Using ContraMSet[T] directly as the parameter type would therefore put

T

positively and fail the variance-position rule. Introduce

U <: T

: both operands can count every U, and their sum is a ContraMSet[U]. This is a restriction to a common query domain; operations do not promise to preserve counts outside the narrowed domain.^[ref]

Pointwise evaluation gives

f_{insert (x)} (y) = f (y) + [y = x], f_{delete (x)} (y) = max (0, f (y) - [y = x]), f_{M union K} (y) = f_{M} (y) + f_{K} (y) .

No old function is modified, so updates preserve immutable object. Constructing each wrapper takes constant work, but a later count may traverse a chain of previously created programming closures; its running time need not be constant in the history length. This functional representation trades enumeration and direct storage of occurrences for composable counting behavior.

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

Separate integer partitions according to whether they contain a part equal to

i

. Removing one such part is a bijection to partitions of

n - i

whose parts are at most

i

. The alternatives are disjoint, giving

p (i, n) = p (i - 1, n) + p (i, n - i) (i \geq 1, n \geq 1) .

Use

p (i, 0) = 1

, because the empty integer partition is counted once, and

p (0, n) = 0

for

n > 0

, with

p (i, n) = 0

for

n < 0

. This Oberon implementation avoids negative recursive arguments:

PROCEDURE P(i, n: INTEGER): INTEGER;
VAR answer: INTEGER;
BEGIN
  IF n = 0 THEN answer := 1
  ELSIF i = 0 THEN answer := 0
  ELSIF i > n THEN answer := P(i-1, n)
  ELSE answer := P(i-1, n) + P(i, n-i)
  END;
  RETURN answer
END P;

PROCEDURE Partitions(n: INTEGER): INTEGER;
BEGIN
  RETURN P(n, n)
END Partitions;

The precondition is

i, n \geq 0

. Each recursive call reduces

i + n

, proving algorithm termination. Every positive part of a partition of

n

is at most

n

, so the required one-argument count is $P (n, n)$ . Counts require a sufficiently wide integer representation.

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Imperative programming (resit) / 3 / b / Solution 2026-10-31

For the paper's 26-letter alphabet, use the Oberon CAP operation and contiguous character codes:

PROCEDURE Index(c: CHAR): INTEGER;
BEGIN
  RETURN ORD(CAP(c)) - ORD("A")
END Index;

Both cases of a letter map to the same uppercase letter before subtraction, so the result lies in 0..25. This relies on the ordinary Latin A–Z and a–z character encoding used by Oberon; it is not a Unicode case-folding algorithm. The stipulated letter-only precondition avoids any need to reject punctuation.

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

Generate each reciprocal factorial from the preceding one, instead of recomputing a factorial for every summand:

def eb(n: Int): Double = {
  require(n >= 0)
  var i = 0
  var term = 1.0
  var sum = 1.0
  while (i < n) {
    i += 1
    term /= i.toDouble
    sum += term
  }
  sum
}

The loop invariant is

0 \leq i \leq n

t er m = 1/ i!

, and

s u m = \sum_{j = 0}^{i} 1/ j!

. Initially

i = 0

and

0! = 1

. The division produces

1/ (i + 1)!

, which is then added to the previous partial sum. The loop variant is

n - i

. Consequently the returned value is $e_{b} (n)$ , using exactly

n

divisions and

n

additions, no multiplications, and

O (n)

time complexity. The slightly weaker precondition also permits the useful zero-term boundary case. For Double, small positive terms eventually cease to change sum because of floating-point rounding.

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

Return the lower-bound search boundary, permitting both zero and the array length:

def lowerBound(a: Array[Int], x: Int): Int = {
  require(a != null) // a is nondecreasing
  var lo = 0
  var hi = a.length
  while (lo < hi) {
    val mid = lo + (hi - lo) / 2
    if (a(mid) < x) lo = mid + 1
    else hi = mid
  }
  lo
}

The precondition includes nondecreasing order. The loop invariant is

0 \leq l o \leq hi \leq n, a [0.. l o) < x, x \leq a [hi .. n) .

Initially both excluded ranges are empty. If

a (mi d) < x

, sortedness justifies excluding every position through mid; otherwise it justifies excluding every position from mid onwards. The loop variant

hi - l o

is a nonnegative integer that strictly decreases. When the old width is positive, mid is a valid array index. The midpoint expression avoids adding two potentially large indices. At exit

l o = hi

, so lo satisfies the required partition, including when

n = 0

. Each new width is at most half the old width, rounded down; this gives

O (lo g (n + 1))

time complexity and constant space, conventionally

O (lo g n)

for nontrivial sizes.

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

Black-box testing chooses inputs and expected outputs from the public specification without using the implementation's control structure. Equivalence class testing partitions the input space into classes expected to exercise similar specified behavior, then chooses representatives; boundary cases test where that behavior changes. For equal-range search, use these concrete representatives:

Empty array: ([], 4) gives (0,0).
One entry, with the target below, equal, and above it: ([4],3), ([4],4), ([4],5) give (0,0), (0,1), (1,1).
An absent interior value: ([1,3,5],4) gives (2,2).
One interior match: ([1,3,5],3) gives (1,2).
A repeated interior block: ([1,3,3,3,5],3) gives (1,4).
A repeated block touching the left or right boundary: ([3,3,5],3) and ([1,3,3],3) give (0,2) and (1,3).
Every entry equal: ([3,3,3],3) gives (0,3); targets two and four give (0,0) and (3,3).
Extreme keys: ([Int.MinValue,0,Int.MaxValue],Int.MaxValue) gives (2,3), and searching for Int.MinValue gives (0,1).

For each result independently check

0 \leq i \leq j \leq n

, the strict inequalities outside the returned interval, and equality inside it. Unsorted inputs violate the precondition; they are not ordinary members of the specified valid-input classes. Software testing supplies evidence about implementations, while the loop invariant proof explains correctness for every valid input.

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

The runtime precondition check rules out negative dimensions:

def makeZeroVector(size: Int): Node = {
  require(size >= 0)
  val h = new Node(0.0, size)
  h.prev = h
  h.next = h
  h
}

Both links point to the fresh list header, so all reciprocal-link conditions hold and there are no ordinary entries to violate ordering or nonzero-value requirements. The abstraction function therefore yields the zero vector of dimension size. Construction uses constant time and constant space.

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

Assume vector already satisfies the full representation invariant in part (b). Check the local bounds and value preconditions, then find the first index not smaller than the requested one:

def setElement(vector: Node, value: Double, index: Int): Unit = {
  require(vector != null)
  require(0 <= index && index < vector.index)
  require(value != 0.0 && !java.lang.Double.isNaN(value) &&
          !java.lang.Double.isInfinite(value))
  var p = vector.next
  while ((p ne vector) && p.index < index) p = p.next
  if ((p ne vector) && p.index == index) p.value = value
  else {
    val left = p.prev
    val fresh = new Node(value, index, left, p)
    left.next = fresh
    p.prev = fresh
  }
}

The search loop invariant says that the structure is unchanged and every ordinary linked list node passed has index smaller than index; p is the next candidate. The number of unpassed ordinary entries is a loop variant. The short-circuit evaluation prevents testing the header index as an ordinary entry. If an equal index exists, changing only its nonzero value preserves the representation invariant. Otherwise left and p delimit the unique insertion position: initializing both new links before redirecting their neighbors preserves reciprocal links and strict index order. Exactly the requested coordinate changes. With

k

stored entries, the search costs

O (k + 1)

and the splice costs constant time; checking the whole input structure is a caller obligation, rather than an unmentioned scan inside each call.