抽象化関数が操作と可換なら実装は仕様を満たす

抽象仕様として、抽象値の集合 $A$、初期値 $a_0 \in A$、各 $m \in \mathrm{Op}$ の事前条件 $\mathrm{pre}^A_m \subseteq A \times X_m$ と写像 $\mathrm{op}^A_m : A \times X_m \to A \times Y_m$ が与えられているとする。データ型の実装 $(\mathrm{Rep}, \mathrm{Init}, (\mathrm{op}_m))$、表現不変条件 $\mathrm{Inv}$、抽象化関数 $\alpha : \mathrm{Inv} \to A$ が次を満たすとする。

• （初期値）$\mathrm{Init} \subseteq \mathrm{Inv}$ で、すべての $r \in \mathrm{Init}$ について $\alpha(r) = a_0$。
• （可換性）すべての $m$、$r \in \mathrm{Inv}$、$x \in X_m$ について、$(\alpha(r), x) \in \mathrm{pre}^A_m$ かつ $\mathrm{op}_m(r, x) = (r', y)$ ならば、$r' \in \mathrm{Inv}$ かつ $\mathrm{op}^A_m(\alpha(r), x) = (\alpha(r'), y)$。

操作の列 $(m_1, x_1), \ldots, (m_N, x_N)$ を、抽象仕様の側で $a_0$ から順に実行した抽象値と結果を $a_i$、$y^A_i$（$\mathrm{op}^A_{m_i}(a_{i-1}, x_i) = (a_i, y^A_i)$）とし、各段で事前条件 $(a_{i-1}, x_i) \in \mathrm{pre}^A_{m_i}$ が成り立つとする。同じ列を実装の側で $r_0 \in \mathrm{Init}$ から順に実行した表現と結果を $r_i$、$y_i$（$\mathrm{op}_{m_i}(r_{i-1}, x_i) = (r_i, y_i)$）とする。このとき、すべての $i$ について

が成り立つ。すなわち、呼び出し側が観測する結果の列は、抽象仕様のものと一致する。