= Abstraction function
{title2=$\alpha:R_{\mathrm{valid}}\to Q$}
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>.<6.005 Software Construction, Spring 2016/Reading 13: Abstraction Functions & Rep Invariants>[Rep Invariant and Abstraction Function: representation space, abstract space, partial AF and boolean RI]{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>.
Back to article page
