模倣関係と操作列のテスト

データ型の実装 $(\mathrm{Rep}, \mathrm{Init}, (\mathrm{op}_m))$ と、参照モデル（抽象仕様）$(A, a_0, (\mathrm{pre}^A_m), (\mathrm{op}^A_m))$ が与えられているとする（記号は 定義 6.1［契約による設計］ と 命題 6.4［契約による設計］ のもの）。表現不変条件 $\mathrm{Inv}$ と抽象化関数 $\alpha : \mathrm{Inv} \to A$ の組であって、命題 6.4［契約による設計］ の（初期値）と（可換性）を満たすものを、実装とモデルのあいだの模倣関係と呼ぶ。

1. 模倣関係が存在するならば、モデルの側で事前条件を満たすどんな操作の列についても、実装の返す結果の列はモデルの返す結果の列と一致する。
2. ある操作の列（モデルの側で事前条件を満たすもの）で、実装の結果とモデルの結果が食い違うならば、模倣関係は存在しない。すなわち、（初期値）を満たすどんな $(\mathrm{Inv}, \alpha)$ についても、（可換性）がどこかで破れている。