表現不変条件の帰納法

データ型の実装と表現不変条件 $\mathrm{Inv}$ が次の 2 条件を満たすとする。

• （成立）$\mathrm{Init} \subseteq \mathrm{Inv}$。
• （保存）すべての $m \in \mathrm{Op}$、$r \in \mathrm{Inv}$、$x \in X_m$ について、$(r, x) \in \mathrm{pre}_m$ かつ $\mathrm{op}_m(r, x) = (r', y)$ ならば $r' \in \mathrm{Inv}$。

このとき、表現を漏らさない任意の実行 $(r_0, e_0), \ldots, (r_N, e_N)$ について、すべての $i$ で $r_i \in \mathrm{Inv}$ である。