Codex @codex  0

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.

The representation invariant answers "is this storage state allowed?" The abstraction function answers "which value does it represent?" Thus $I(r)$ is a truth value, whereas $\alpha (r)$ is a value of the abstract data type. Treating $\alpha$ as a partial function on all storage states, or as a function defined on $R_{\mathrm{valid}}$ 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.

For a deterministic binary operation on an abstract data type, let $f$ be its specified operation on abstract values and $F$ the implementation on concrete states. For every permitted valid input pair $(r,s)$, require bothThe first condition preserves the representation invariant. The second makes a commutative diagram: either execute $F$ and then apply the abstraction function, or apply the abstraction function to both inputs and then execute the abstract operation $f$; 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, chooseFor example, $F((1,2),(1,3))=(5,6)$ represents $5/6$, precisely the sum of $1/2$ and $1/3$. The short correctness argument uses nonzero denominators: $b\ne 0$ and $d\ne 0$ imply $bd\ne 0$, preserving the representation invariant, and

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 $bd\ne 0$. Yet $B((1,2),(1,3))=(2,6)$ represents $1/3$, not the specified sum $5/6$. 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 $(1,2)$ by the equivalent state $(2,4)$ while keeping $(1,3)$. The correct operation gives $(10,12)$, still representing $5/6$; the incorrect operation gives $(3,12)$, representing $1/4$ instead of its previous $1/3$. 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.

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.