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 iswith 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.
private var last: Node = nullNull 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.A sufficient representation invariant is:
The abstraction function isThe 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 2026-10-13
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.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
Sparse linked vector representation 2026-10-31
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.
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.
Unreduced rational representation 2026-10-14
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 areThe 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.
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]
8.3 Module Documentation. Section 8.3.1, Abstraction Functions: several concrete values mapping to one abstract value; Section 8.3.4, Representation Invariants: valid domain of AF



