契約：事前条件と事後条件

状態（変数の値の割り当て）の集合を $\Sigma$ とする。$\Sigma$ の部分集合を表明という。表明 $P$ と状態 $\sigma$ について、$\sigma \in P$ を $P(\sigma)$ とも書き、「$\sigma$ で $P$ が成り立つ」と読む。

操作 $m$ の契約とは、表明の組 $(P, Q)$ をいう。$P$ を事前条件、$Q$ を事後条件という。契約 $(P, Q)$ は次の約束を表す。

• 呼び出し側の義務: $P$ が成り立つ状態でだけ $m$ を呼ぶ。
• 実装側の義務: $P$ が成り立つ状態から実行を始めて止まったなら、止まった状態で $Q$ が成り立つ。

表明 $P, P'$ について、$P \subseteq P'$ のとき $P \Rightarrow P'$ と書き、$P$ は $P'$ より強い、$P'$ は $P$ より弱いという。$P \wedge P' = P \cap P'$、$P \vee P' = P \cup P'$、$\lnot P = \Sigma \setminus P$、$\mathrm{true} = \Sigma$、$\mathrm{false} = \emptyset$ と書く。