データ型の実装・表現不変条件・抽象化関数

データ型の実装とは、次の組 $(\mathrm{Rep}, \mathrm{Init}, (\mathrm{op}_m)_{m \in \mathrm{Op}})$ をいう。

• $\mathrm{Rep}$ は表現（内部の状態）の集合、$\mathrm{Init} \subseteq \mathrm{Rep}$ は構築子が作りうる表現の集合。
• 各公開操作 $m \in \mathrm{Op}$ は、引数の集合 $X_m$、結果の集合 $Y_m$、事前条件 $\mathrm{pre}_m \subseteq \mathrm{Rep} \times X_m$ と、写像 $\mathrm{op}_m : \mathrm{Rep} \times X_m \to \mathrm{Rep} \times Y_m$（新しい表現と結果を返す）をもつ。

表現不変条件とは、部分集合 $\mathrm{Inv} \subseteq \mathrm{Rep}$ をいう。集合 $A$（抽象値の集合）への写像 $\alpha : \mathrm{Inv} \to A$ を抽象化関数という。

このデータ型を使うプログラムの実行とは、表現と呼び出し側の状態の組の列 $(r_0, e_0), (r_1, e_1), \ldots, (r_N, e_N)$ をいう。実行が表現を漏らさないとは、$r_0 \in \mathrm{Init}$ であり、各 $i \lt N$ について次のどちらかが成り立つことをいう。

• （公開操作の呼び出し）ある $m \in \mathrm{Op}$ と $x \in X_m$ があって、$(r_i, x) \in \mathrm{pre}_m$ かつ $\mathrm{op}_m(r_i, x) = (r_{i+1}, y)$（$y$ は結果）。
• （呼び出し側の動作）$r_{i+1} = r_i$。