Codex @codex  0

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]

An abstraction function maps a valid concrete representation to its abstract value. Write $R_{\mathrm{valid}}=\{r:I(r)\}$ and $\alpha :R_{\mathrm{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.

Consider an original FIFO queue example storing immutable labels, with fixed positive integer capacity $C$. Its abstract state is a finite sequence $q=(x_0,\dots ,x_{n-1})$, with $0\le n\le C$. 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 $n$. The status results are distinct from stored labels.

For a compact array representation $(A,n)$, fix $|A|=C$ and require the representation invariantThe abstraction function is $\alpha (A,n)=(A_0,\dots ,A_{n-1})$. Only these first $n$ entries matter; unused slots have no abstract meaning. On successful enqueue(x), write $A_n=x$ and then set $n\leftarrow n+1$. On successful dequeue(), save $A_0$, shift the remaining $n-1$ entries left, and decrement $n$. Testing the full or empty case before updating gives the specified unchanged failure state.

With $C=3$ and $q=(A,B)$, enqueue(C) produces $(A,B,C)$; enqueue(D) returns full without change. A raw write $n\leftarrow 4$ violates the representation invariant. More subtly, changing the count from two to one satisfies its bounds but discards $B$ 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.

Encapsulation bundles related program state and operations or hides implementation details behind an interface. Encapsulation in object-oriented programming realizes this through objects and their permitted operations; encapsulation also applies to modules outside object-oriented programs.

The useful boundary is a promise: clients request operations through an API, and the implementation maintains a representation invariant. Instead of proving that every client updates several storage fields consistently, prove that the permitted operations preserve the representation invariant. Information hiding also leaves room to replace the data structure while keeping the client-facing behavior, a property called representation independence.

Bundling state and operations alone does not establish that promise. Representation exposure can let clients bypass the API. A private annotation alone is not a security guarantee: it does not establish correctness of operations, isolation from hostile code or safe handling of shared mutable storage. The examples below concern sequential calls with no concurrent access and no client access to internal storage; they do not claim protection against arbitrary memory modification.

Representation exposure gives outside code access that can modify storage on which the representation invariant or promised behavior depends. Returning the internal array exposes a route around the API; merely hiding the field name does not close it. Incoming shared mutable storage can create the same problem. Copies or immutable values can prevent such modification, but their costs and sharing rules belong in the design.^[ref]

The bounded queue with encapsulation deliberately stores immutable labels. A FIFO queue of mutable objects needs a separate promise about whether changing a returned object changes stored content; protecting the queue's ordering and size does not automatically make every stored object immutable.

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 $B$, front index $h$ and count $n$. Its representation invariant is $|B|=C$, $h,n\in \mathbb{Z}$, $0\le h<C$ and $0\le n\le C$. Its abstraction function reads the occupied slots using modular arithmetic:On successful enqueue(x), write $B_{(h+n)\mathrm{mod}C}=x$ and increment $n$. On successful dequeue(), return $B_h$, replace $h$ by $(h+1)\mathrm{mod}C$ and decrement $n$. 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 $C=3$, start empty, enqueue $A,B,C$, dequeue twice, enqueue $D,E$, try to enqueue $F$, then peek and size. Both implementations return $A,B$ from the removals, report full for $F$, and finish with front $C$, size three and abstract sequence $(C,D,E)$. The compact array stores $(C,D,E)$ from index zero; the circular buffer stores $(D,E,C)$ with $h=2$. 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 $n-1$ slot moves on a successful removal: $O(n)$ worst-case time complexity as capacity varies. The circular buffer does no slot moves and uses $O(1)$ worst-case time complexity for all four operations. Both allocate $C$ 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.

A representation invariant $I(r)$ specifies which concrete storage states $r$ are valid at the API boundary. Construction must establish it, and each completed operation must preserve it. Internal steps may temporarily violate it only while that state is inaccessible to observers; callbacks or concurrent access would require further reasoning.^[ref]

The short proof pattern is mathematical induction on the number of completed calls: the initial state satisfies $I$; every permitted transition from an $I$-state ends in an $I$-state; hence every state observable through the API satisfies $I$. An unrestricted external write falls outside this argument.