表明への代入

定義 3.4（「契約による設計」§3）

表明 $Q$ 、変数 $x$ 、算術式 $a$ に対して、表明 $Q[a/x]$ を

Q[a/x] = \{\, \sigma \in \Sigma \mid Q(\sigma[x \mapsto \llbracket a \rrbracket\sigma]) \,\}

で定める。また、算術式 $a'$ とブール式 $b$ の中の変数 $x$ をすべて $a$ に書き換えた式を $a'[a/x]$ 、 $b[a/x]$ と書く。

閉包の状態

定義

定義は閉包の起点です（証明を要しません）。

印の意味: ✓公理まで証明済み・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は閉包の状況。