Save the next pointer before redirecting it, then advance the two working heads. No node is allocated and the name/number fields are untouched.
def reverseBook(): Unit = {
  var prev: Node = null
  var cur = list
  while (cur != null) {
    val following = cur.next
    cur.next = prev
    prev = cur
    cur = following
  }
  list = prev
}
Let be the original sequence of node identities, not just their possibly equal field values. Write for the sequence currently headed by prev and for that headed by cur. A suitable loop invariant for in-place linked-list reversal is
with both working lists finite, acyclic, disjoint, together containing exactly the original nodes, and with every name and number unchanged. Here ++ means concatenation. Initially and . One iteration takes from the front of and replaces by . Since , the equation is preserved. Saving following before changing cur.next retains access to .
The loop variant is the length of , decreasing by one. At exit , so ; assigning the head establishes reversal. The empty and singleton cases work without a special branch. The abstraction function of the phone book ignores order, so it still maps every original name to its original number. All original node identities are reused, with running time and auxiliary space.
Figure 1.
In-place reversal preserves node identities while moving nodes from an untouched suffix into a reversed prefix
. Details.
Use a non-dummy circular linked list with a pointer to its last node:
private var last: Node = null
Null represents the empty book. In a nonempty book, last.next is the first node, and following next makes one finite simple cycle containing last. Names are unique around that cycle. This representation makes appending a new entry constant-time once a failed name search has established absence. The abstraction function collects every name/number pair on one complete turn of the cycle, rather than following pointers until null.
  • Both arrays have length capacity, with and .
  • The active keys elements(0 until used) are pairwise distinct.
  • For each active index , representatives(k) equals some active key elements(j).
  • Every such representative is fixed: if representatives(k) == elements(j), then representatives(j) == elements(j).
The abstraction function is
The last two conditions ensure each representative is a genuine member of its own block and that the abstract function is idempotent function. Cells beyond used are unconstrained and ignored. When used == 0, these conditions hold vacuously and the abstraction function yields the empty map. This is an explicit-key version of quick-find, rather than a parent-pointer disjoint-set forest.
Quick-find 2026-10-24
An eager representation of a disjoint-set data structure that stores each member's current representative directly. Finding a representative is direct when keys are array indices; arbitrary keys in a parallel key array can add a linear search. A disjoint-set union operation scans members and replaces every occurrence of one old representative with the other. The representative labels must be snapshotted before this scan. Its easy abstraction function contrasts with the parent-pointer representation of a disjoint-set forest.
Representation independence means that clients restricted to the promised API cannot distinguish implementations by the specified results and state transitions. State what observations count: equal returned labels and failure statuses do not imply equal running times, allocations or physical layouts. If the API also promises a resource bound, a replacement must meet that bound too.
Replace the compact array in the bounded queue with encapsulation by a circular buffer with storage , front index and count . Its representation invariant is , , and . Its abstraction function reads the occupied slots using modular arithmetic:
On successful enqueue(x), write and increment . On successful dequeue(), return , replace by and decrement . Full and empty failures do not alter storage. peek and size have the same abstract meanings as before. Keeping a count distinguishes a full circular buffer from an empty one even when both would have the same next insertion index.
Figure 1.
The same bounded queue trace uses shifting array storage or a wrapping circular buffer
. Details.
For , start empty, enqueue , dequeue twice, enqueue , try to enqueue , then peek and size. Both implementations return from the removals, report full for , and finish with front , size three and abstract sequence . The compact array stores from index zero; the circular buffer stores with . Their abstraction functions explain why different stored entries describe the same ordered content.
Under constant-cost slot access and index arithmetic, with no resizing and labels that fit in one slot, the compact array does slot moves on a successful removal: worst-case time complexity as capacity varies. The circular buffer does no slot moves and uses worst-case time complexity for all four operations. Both allocate slots initially; that construction cost is separate. These are operation-count claims in Big O notation, not measured timings. The short correctness outline checks that each implementation's abstraction function produces the specified new sequence and return value after every successful or rejected call. Repeating that check gives equal traces for clients using only this API.
Sentinel node 2026-10-24
A sentinel is a permanently present linked list node that is excluded from the represented data. A header sentinel provides a predecessor even for the first real element, allowing uniform link updates. Its datum has no abstract meaning and must not be counted by the abstraction function. A representation invariant should keep the sentinel outside its own finite acyclic successor chain.
Shared-array double stack Created 2026-10-24 Updated 2026-10-31
Two stacks can share a fixed array by growing inwards from opposite ends. Store one stack in and the other in , with representation invariant . The first top is at , the second at , and is free. The abstraction function reads the first segment backwards and the second forwards to obtain top-first lists. Push requires ; 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.
Represent a finite sparse vector by a sorted doubly linked list of its nonzero coordinates. A list header stores the dimension; every ordinary linked list node stores a distinct valid coordinate index, its nonzero value, and predecessor and successor references. In a circular linked list, the endpoints connect to the header, and an all-zero vector has the header linked to itself in both directions. The representation invariant requires strictly increasing ordinary indices, valid bounds and mutually consistent forward and backward links. The abstraction function assigns zero to every coordinate absent from the list. The header is metadata, never an ordinary coordinate.
For example, has dimension nine and only three stored coordinates. The header's index field can store nine even though nine is not a valid coordinate index. Keeping the header distinct is therefore essential when searching for or removing entries.
Figure 1.
A circular sparse linked vector representation stores only nonzero coordinates
. Details.
Sparse map with a default value Created 2026-10-24 Updated 2026-10-31
Represent a total function by storing only selected entries of a finite partial function and returning a fixed default for missing keys. A missing payment-count record can denote two zero counts. Storing an explicit default-valued record can have the same observable meaning, so the abstraction function need not be injective. Update operations must preserve all unrelated keys and establish the intended change whether or not the key was previously stored.
Consider an original abstract data type whose values are rational numbers. Store an ordered pair 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
The representation invariant does not require a positive denominator or a reduced fraction. Consequently , and are three different concrete states with the same abstract rational number . Similarly, and 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 and violate the representation invariant; neither has a value under this abstraction function. By contrast, is completely valid. Simplifying it to the reduced fraction 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 and ,
This defines an equivalence relation on : 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 and unequal as rational numbers. The general reason is that an abstraction function may map several concrete values to one abstract value.[ref]