= Bounded queue with encapsulation
{title2=$0\leq |q|\leq C$}
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,\ldots,x_{n-1})$, with $0\leq n\leq 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 invariant>
$$
I(A,n):\quad n\in\mathbb Z,\qquad 0\leq n\leq C.
$$
The <abstraction function> is $\alpha(A,n)=(A_0,\ldots,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.
\Image[/encapsulated-queue-api-state-boundary.png]
{title=Permitted queue calls preserve valid states; an unrestricted count write bypasses the API}
With $C=3$ and $q=(A,B)$, `enqueue(C)` produces $(A,B,C)$; `enqueue(D)` returns `full` without change. A raw write $n\leftarrow4$ 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.
Back to article page
