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.