情報科学 › ソフトウェア設計とテスト › 契約による設計

最弱事前条件

定義 4.1（「契約による設計」§4）

解釈 M\mathcal{M}、命令 cc、表明 QQ に対して

wlp(c,Q)={ σ∣すべての σ′ について、⟨c,σ⟩⇓σ′ ならば Q(σ′) },wp(c,Q)={ σ∣c は σ から停止し、すべての σ′ について、⟨c,σ⟩⇓σ′ ならば Q(σ′) }\begin{aligned} \mathrm{wlp}(c, Q) &= \{\, \sigma \mid \text{すべての } \sigma' \text{ について、} \langle c, \sigma \rangle \Downarrow \sigma' \text{ ならば } Q(\sigma') \,\}, \\ \mathrm{wp}(c, Q) &= \{\, \sigma \mid c \text{ は } \sigma \text{ から停止し、すべての } \sigma' \text{ について、} \langle c, \sigma \rangle \Downarrow \sigma' \text{ ならば } Q(\sigma') \,\} \end{aligned}

と定める。wlp(c,Q)\mathrm{wlp}(c, Q) を最弱自由事前条件（weakest liberal precondition）、wp(c,Q)\mathrm{wp}(c, Q) を最弱事前条件（weakest precondition）という。

本文で読む（前後の説明と例）→

閉包の状態

定義

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

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

これを使っている定理

証明で明示的に参照している定理は、まだありません。