 Bounded queue with encapsulation

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.