契約の精密化（振る舞いの部分型）

$\mathcal{C}, \mathcal{C}'$ を契約表（定義 3.7）とする。すべての $(m, P, Q) \in \mathcal{C}$ に対して、

を満たす $(m, P', Q') \in \mathcal{C}'$ が存在するとき、$\mathcal{C}'$ は $\mathcal{C}$ を精密化するという。$\mathcal{C}$ を上位型の契約、$\mathcal{C}'$ を下位型の契約とみるとき、下位型は上位型の振る舞いの部分型であるという。