= Correct operations through an abstraction function
{title2=$\alpha(F(r,s))=f(\alpha(r),\alpha(s))$}
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 both
$$
I(F(r,s))\qquad\text{and}\qquad \alpha(F(r,s))=f(\alpha(r),\alpha(s)).
$$
The 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>.<OCaml Programming: Correct + Efficient + Beautiful by Michael R. Clarkson and others/8.3 Module Documentation>[Sections 8.3.3, Commutative Diagrams, and 8.3.4, Representation Invariants: matching abstract results and preservation of valid representations]{ref}
For <addition> in the <unreduced rational representation>, choose
$$
f(x,y)=x+y,\qquad F((a,b),(c,d))=(ad+bc,bd).
$$
For 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\ne0$ and $d\ne0$ imply $bd\ne0$, preserving the <representation invariant>, and
$$
\alpha(F((a,b),(c,d)))=\frac{ad+bc}{bd}=\frac ab+\frac cd=f(\alpha(a,b),\alpha(c,d)).
$$
\Image[/rational-addition-commuting-counterexample.png]
{title=Correct rational addition makes both paths agree; an invariant-preserving incorrect operation gives a different value}
Now consider an incorrect implementation that uses <addition> on the <numerators> and <multiplication> on the <denominators>:
$$
B((a,b),(c,d))=(a+c,bd).
$$
It preserves the <representation invariant> for every valid <input> pair because its <denominator> is still $bd\ne0$. 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.
Back to article page
