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]
Abstract data type invariant Created 2026-10-24 Updated 2026-10-31
A condition describing legal abstract states, independently of their concrete storage. A bounded-key multiset has nonnegative counts and zero counts outside its allowed range. A representation invariant instead constrains implementation states; an abstraction function connects a valid representation to its abstract state. The two kinds of invariant should not be conflated.
Abstraction function Created 2026-10-13 Updated 2026-10-14
An abstraction function maps a valid concrete representation to its abstract value. Write and . 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 is a truth value, whereas is a value of the abstract data type. Treating as a partial function on all storage states, or as a function defined on 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.
Array multiset Created 2026-10-25 Updated 2026-10-31
A multiset of keys in a fixed finite integer range represented by one nonnegative count per key. The abstraction function extends the stored array counts by zero outside the range. Single-key additions, removals and queries use constant array work, provided overflow and operation preconditions are handled. Encapsulation of the count array is necessary to preserve its representation invariant.
Consider an original FIFO queue example storing immutable labels, with fixed positive integer capacity . Its abstract state is a finite sequence , with . The API has enqueue(x), dequeue(), peek() and size(). Successful enqueue returns ok; a full queue returns full and is unchanged. Successful dequeue returns the first label and removes it; an empty queue returns empty and is unchanged. peek returns the first label or empty without modification, and size returns . The status results are distinct from stored labels.
For a compact array representation , fix and require the representation invariant
The abstraction function is . Only these first entries matter; unused slots have no abstract meaning. On successful enqueue(x), write and then set . On successful dequeue(), save , shift the remaining entries left, and decrement . Testing the full or empty case before updating gives the specified unchanged failure state.
Figure 1.
Permitted queue calls preserve valid states; an unrestricted count write bypasses the API
. Details.
With and , enqueue(C) produces ; enqueue(D) returns full without change. A raw write violates the representation invariant. More subtly, changing the count from two to one satisfies its bounds but discards without a permitted operation. Validity of the storage state and legality of the API transition are different obligations. A setter for every storage field would surrender the useful boundary even if its name looked like an ordinary operation.
Circular buffer Created 2026-10-13 Updated 2026-10-18
A circular buffer stores a changing sequence in a fixed-capacity array, reusing slots by wrapping array indices through modular arithmetic. A front array index and an occupied count can represent a FIFO queue without shifting entries after removal. The physical array stays in place; the position at which its logical sequence begins moves. This makes a circular buffer useful when storage must remain bounded while successive items arrive and leave.
Capacity and overflow behavior are separate choices. A rejecting FIFO queue preserves all accepted items until removal and reports failure on a full insertion. An overwriting circular buffer deliberately discards its oldest item to retain the newest arrivals. These are different application programming interfaces. The existing representation independence example specifies the rejecting policy and gives its abstraction function and correctness argument against a shifting array implementation.
Start with , , and immutable labels. Perform enqueue(A), enqueue(B), dequeue(), enqueue(C), enqueue(D), dequeue(), enqueue(E), enqueue(F), enqueue(G). The removals return and . The interleaved insertions and removals make the front advance before the array fills; slot reuse does not require waiting for the FIFO queue to become empty.
Figure 1.
An interleaved capacity-five FIFO queue trace branches at a full insertion
. The table follows completed sequential calls. At step 10, rejecting retains ; overwriting accepts and discards . Step 11 therefore returns different labels. The lower bars show membership lifetimes for and at operation boundaries, not elapsed times or programming-language object lifetimes. Details.
At step 7, occupies physical slot and the next-write array index wraps to . At step 8, reuses slot , giving the physical layout in the preceding diagram. At step 9, replaces the stale contents of slot : the physical array is but the logical sequence is . Now , yet makes the state full rather than empty.
The displayed values are related by after every call. They are shown together to explain the invariant; an implementation need store only two. For the rejecting FIFO queue, every successful removal returns the earliest accepted label not already removed. The representation independence example supplies the general proof through its abstraction function; this trace makes the wrapped physical storage visible.
For a deterministic binary operation on an abstract data type, let be its specified operation on abstract values and the implementation on concrete states. For every permitted valid input pair , require both
The first condition preserves the representation invariant. The second makes a commutative diagram: either execute and then apply the abstraction function, or apply the abstraction function to both inputs and then execute the abstract operation ; 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
For example, represents , precisely the sum of and . The short correctness argument uses nonzero denominators: and imply , preserving the representation invariant, and
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:
It preserves the representation invariant for every valid input pair because its denominator is still . Yet represents , not the specified sum . 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 by the equivalent state while keeping . The correct operation gives , still representing ; the incorrect operation gives , representing instead of its previous . 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.
Keep the physical doubly linked list unchanged and represent the logical sequence in either forward or backward order according to a Boolean flag. Toggling the flag reverses the logical contents in constant time complexity. Endpoint insertion and indexed access must interpret their positions using the flag, and the abstraction function explicitly accounts for this choice.
For an order ideal in a finite rectangular grid with coordinatewise partial order, occupied cells in each row form a left prefix. Their lengths form a nonincreasing sequence . Conversely, any nonincreasing sequence of valid row lengths specifies exactly one such order ideal, giving an abstraction function with no redundant per-cell information.
Removing all occupied cells with and replaces by for and leaves earlier rows unchanged. The new lengths remain nonincreasing: affected rows preserve their mutual order, and the first affected row only decreases. For a legal removal, the boundary immediately below it was already at least . A cached sum of row lengths can be updated by subtracting the decreases. This yields constant-time membership and count queries, linear storage, and an update linear in the number of affected rows.
Place these methods inside the LLBuffer class. The two private insertion methods operate on physical endpoints; the public methods interpret logical endpoints using the reversal flag.
private def addFirst(x: Int): Unit = {
  val q = new Node(x)
  q.next = first
  if (first == null) last = q else first.prev = q
  first = q
  size += 1
}

private def addLast(x: Int): Unit = {
  val q = new Node(x)
  q.prev = last
  if (last == null) first = q else last.next = q
  last = q
  size += 1
}

def append(x: Int): Unit = {
  if (backwards) addFirst(x) else addLast(x)
}

def prepend(x: Int): Unit = {
  if (backwards) addLast(x) else addFirst(x)
}

def get(i: Int): Int = {
  require(0 <= i && i < size)
  val j = if (backwards) size - 1 - i else i
  var q: Node = null
  if (j <= size - 1 - j) {
    q = first
    var k = 0
    while (k < j) { q = q.next; k += 1 }
  } else {
    q = last
    var k = size - 1
    while (k > j) { q = q.prev; k -= 1 }
  }
  val x = q.value
  if (q.prev == null) first = q.next else q.prev.next = q.next
  if (q.next == null) last = q.prev else q.next.prev = q.prev
  q.prev = null
  q.next = null
  size -= 1
  x
}

def rev: Unit = { backwards = !backwards }
In the forward traversal, the loop invariant is that q is physical node , with ; its loop variant is . In the backward traversal, q is physical node , with ; its loop variant is . Thus both locate physical index , which is exactly logical index under the abstraction function.
Deletion bypasses the chosen linked list node in both directions. Deleting the first or last linked list node updates the corresponding endpoint; deleting the only linked list node sets both endpoints to null. The surviving values keep their physical relative order, so the abstraction function gives precisely the required logical deletion. Each insertion preserves reciprocal links and adds its value at the physical end corresponding to the required logical end. Toggling the flag changes to its list reversal without moving any linked list nodes. Consequently
These are worst-case time complexity bounds in the constant-cost pointer model; total storage is and each operation uses constant auxiliary space.
Use a doubly linked list, store both physical endpoints and its length, and maintain a flag for lazy reversal of a doubly linked list. This makes endpoint insertion and reversal constant time. Finding an arbitrary indexed element takes a traversal from whichever physical endpoint is nearer.
class LLBuffer extends ReversableBuffer {
  private class Node(val value: Int) {
    var prev: Node = null
    var next: Node = null
  }
  private var first: Node = null
  private var last: Node = null
  private var size = 0
  private var backwards = false

  // Methods from (ii) go here.
}
Define to be the sequence of values obtained by starting at first and repeatedly following next until null. The representation invariant says that size is nonnegative; size == 0 holds exactly when both endpoints are null; otherwise there are exactly size distinct reachable linked list nodes, the final one is last, first.prev == null, last.next == null, and all neighboring links are reciprocal. These conditions make finite and the physical linked list acyclic. The abstraction function is
The flag does not change the representation invariant. An empty physical linked list represents the empty sequence for either flag value. No client receives a linked list node reference, so clients cannot invalidate its links.
Use a minimum stack: each linked list node caches the minimum of all values from that node down to the bottom. This handles duplicate minima without searching when one is removed.
class Stack {
  private class Node(val value: Int, val least: Int, val next: Node)
  private var top: Node = null

  def push(x: Int): Unit = {
    val m = if (top == null) x else math.min(x, top.least)
    top = new Node(x, m, top)
  }

  def pop(): Int = {
    require(!isEmpty)
    val x = top.value
    top = top.next
    x
  }

  def isEmpty: Boolean = top == null

  def min: Int = {
    require(!isEmpty)
    top.least
  }
}
The representation invariant is that the chain from top is finite and acyclic, and every reachable node q satisfies
The abstraction function takes the values along this chain in top-to-bottom order. Thus pushing changes to , and popping a nonempty returns its head and leaves its tail. The cached-minimum equation follows for a new node from the previously valid chain; removing a head leaves every surviving equation unchanged. Consequently
The bounds use the usual constant-cost allocation and integer arithmetic model. Storage is linear in the number of entries. min and pop require a nonempty stack; min leaves it unchanged.
A prefix-dropping iterator must preserve the first satisfying element. Reading it to test the predicate physically consumes it from the source, so keep it in a one-element buffer. Once a match is found, return the entire suffix without testing subsequent elements again.
trait Iter[T] {
  def hasNext: Boolean
  def next(): T
  def copy(): Iter[T]
}

class DropUntil[T](p: T => Boolean, iter: Iter[T]) extends Iter[T] {
  private var seeking = true
  private var saved: Option[T] = None

  private def prepare(): Unit = {
    if (seeking) {
      while (saved.isEmpty && iter.hasNext) {
        val x = iter.next()
        if (p(x)) saved = Some(x)
      }
      seeking = false
    }
  }

  def hasNext: Boolean = {
    prepare()
    saved.nonEmpty || iter.hasNext
  }

  def next(): T = {
    prepare()
    saved match {
      case Some(x) => saved = None; x
      case None =>
        if (!iter.hasNext) throw new NoSuchElementException("next")
        iter.next()
    }
  }

  def copy(): Iter[T] = {
    val result = new DropUntil[T](p, iter.copy())
    result.seeking = seeking
    result.saved = saved
    result
  }
}
Assume the source iterator is owned by the wrapper, its copy meets the stated independent-cursor contract, and is a pure function. Before preparation, the logical remainder is the source remainder with its maximal initial failing prefix removed. After preparation, it is the buffered match followed by the source remainder, or simply the source remainder when the buffer is empty. This describes the abstraction function and proves that repeated hasNext calls neither lose the match nor skip more values.
Copying preserves the phase flag and optional buffered value and independently copies the source iterator. It does not rerun the predicate on an already accepted match. A shallow copy of the wrapper alone would give shared iterator consumption, violating the specification. Therefore
When no element satisfies , a finite source yields an empty iterator. Seeking can diverge on an infinite source with no match; this is inherent in determining whether its required suffix begins anywhere. An element object is not deep-copied by this cursor operation.
A simple current-value implementation works when is a pure function, but sharing a mutable closure between copies would violate the independence requirement used in part (d). Use a memoized successor chain for stateful iterator copies: the generated sequence has shared cells, and each iterator has its own current-cell pointer.
object FunIter {
  final class Cell[T](val head: T, f: T => T) {
    lazy val tail: Cell[T] = new Cell[T](f(head), f)
  }
}

class FunIter[T](v: T, f: T => T) extends Iter[T] {
  private var cursor = new FunIter.Cell[T](v, f)

  def hasNext: Boolean = true

  def next(): T = {
    val x = cursor.head
    cursor = cursor.tail
    x
  }

  def copy(): Iter[T] = {
    val result = new FunIter[T](cursor.head, f)
    result.cursor = cursor
    result
  }
}
The representation invariant is that cursor points to the next cell to be returned, and each cell's lazy tail is computed at most once. The abstraction function is the infinite sequence of heads starting at that cell. Advancing changes only this iterator's pointer. A copy starts at the same cell, so both observe the same remaining heads even when their calls are interleaved:
For a stateful , the generator state must be privately owned by this shared chain; unrelated external calls to must not change it. As usual, the values and transition must allow successive results to be observed without externally mutating old results. No interface can independently clone the hidden state of an arbitrary externally mutated closure from its function type alone. The chain avoids needing such cloning: a lagging copy reuses the already generated future instead of invoking again.
Each new cell needs one transition and constant bookkeeping, but retained slower copies can keep a long generated prefix alive. This is an intentional space tradeoff that permits the stateful generator in part (d). No output is possible if computing a demanded transition itself fails or diverges.
Represent the set by a private list containing each value once. Normalize the constructor input as well as checking future insertions; otherwise duplicate initial entries would violate the intended set behavior.
class Set[T](contents: List[T]) {
  protected var elems: List[T] = contents.distinct

  def add(x: T): Unit = {
    if (!elems.contains(x)) elems = x :: elems
  }

  def delete(): T = {
    require(elems.nonEmpty)
    val x = elems.head
    elems = elems.tail
    x
  }
}
The representation invariant is that elems contains no duplicates under the chosen stable value equality; the abstraction function forgets its ordering and returns its set of elements. The protected field allows the subclass in part (d) to inspect its contents; that subclass is responsible for preserving the representation invariant if it mutates them.
Insertion makes the represented set . Deletion requires , returns some , and leaves . Thus
Deletion does not promise to choose a minimum. With this linked list representation, insertion takes time complexity because of its membership check, while deletion takes . Values should not mutate in a way that changes their equality while stored.
An immutable object can widen its element type when adding a value by returning a new object. Introduce a lower type bound on the method's fresh type parameter.
class ISet[+T](contents: List[T]) {
  private val elems: List[T] = contents.distinct

  def add[U >: T](x: U): ISet[U] = {
    val widened: List[U] = elems
    if (widened.contains(x)) new ISet[U](widened)
    else new ISet[U](x :: widened)
  }

  def delete(): (T, ISet[T]) = {
    require(elems.nonEmpty)
    (elems.head, new ISet[T](elems.tail))
  }
}
As before, the representation invariant excludes duplicates, and the abstraction function returns the unordered set of entries. The constructor normalization makes the representation invariant hold even for repeated initial entries. Both operations construct a fresh set object and leave the original object unchanged, including when addition finds an existing member.
For a receiver representing , the new object returned by add represents . Deletion returns a pair with and representing . Crucially,
The widened list is valid because immutable List itself has a covariant type parameter. A client can view an ISet[Int] as ISet[Any], but adding a string creates a separate widened result; it cannot put a string into the old integer set. This explains how using immutable objects makes the desired type variance sound. A direct add(x: T) on a covariant software class would still violate the variance-position rule; immutability alone does not repair an incorrectly typed method signature.
Follow the next reference for the desired level, stopping at the tail. This returns the genuine nodes in their linked list order, excluding both sentinel nodes.
def nodesAt(level: Int): List[Node] = {
  require(0 <= level && level < NumLevels)
  val out = scala.collection.mutable.ListBuffer.empty[Node]
  var n = head.nexts(level)
  while (n ne tail) {
    out += n
    n = n.nexts(level)
  }
  out.toList
}
Write for the resulting sequence of nodes at level . The abstraction function is
It preserves repetitions, because distinct nodes may carry equal values. A suitable representation invariant requires the following:
  • head and tail are distinct sentinel nodes with the specified extreme values; every node has a nexts array of length NumLevels.
  • For each level, following references from head gives a finite acyclic chain ending at tail, then null; the data along that chain are nondecreasing. Genuine values lie strictly between the sentinel values.
  • Each is a subsequence of by node identity, so the relative order of equal-valued nodes agrees across levels. Every genuine node occurs in and on a contiguous initial collection of levels.
  • A genuine node absent from a level has null in that level's slot. Tail slots are all null; every other slot on a chain points to the next member of that chain.
These structural requirements make the traversal terminate and make descending through levels valid. A probabilistic height distribution is a performance policy, rather than a condition needed for the abstraction function to describe an ordered sequence.
The representation invariant is , rows.length == N, and every rows(i) is a nonnull finite list of entries satisfying
Strict increase excludes repeated columns. The abstraction function gives when the unique entry occurs in rows(i), and otherwise. Thus omitted positions represent zero; omission does not mean an unknown matrix entry.
Interpret step as a positive increment, consistent with the increasing sequence and exclusive upper bound. State this precondition explicitly; a zero increment would not define the intended finite progression. Use a wider cursor to avoid integer overflow on the update after the last valid Int result.
class RangeIter(lower: Int, upper: Int, step: Int) extends Iter[Int] {
  require(step > 0)
  private var current = lower.toLong
  def hasNext: Boolean = current < upper.toLong
  def next(): Int = {
    require(hasNext)
    val answer = current.toInt
    current += step.toLong
    answer
  }
}
After calls to next, the abstraction function is the sequence of values with , in increasing order. Repeated calls to hasNext do not change it; next removes precisely its first value. Therefore
If lower >= upper, the represented sequence is empty immediately. The paper does not specify a descending-range convention; this implementation exposes its positive-step precondition rather than assigning one implicitly.