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

言語 W

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

Var\mathrm{Var} を変数の集合、Op\mathrm{Op} を操作名の有限集合とする。状態とは写像 σ:Var→Z\sigma : \mathrm{Var} \to \mathbb{Z} をいい、状態の全体を Σ\Sigma と書く。σ[x↦n]\sigma[x \mapsto n] は、xx の値を nn に変え、ほかの変数の値を σ\sigma と同じにした状態を表す。

算術式 aa、ブール式 bb、命令 cc を次の文法で定める（n∈Zn \in \mathbb{Z}、x∈Varx \in \mathrm{Var}、kk は正の整数、m∈Opm \in \mathrm{Op}）。

a::=n∣x∣a1+a2∣a1−a2∣a1×a2∣a1÷kb::=true∣a1=a2∣a1≤a2∣¬b∣b1∧b2c::=skip∣x:=a∣c1;c2∣if b then c1 else c2∣while b do c∣call m\begin{aligned} a &::= n \mid x \mid a_1 + a_2 \mid a_1 - a_2 \mid a_1 \times a_2 \mid a_1 \div k \\ b &::= \mathtt{true} \mid a_1 = a_2 \mid a_1 \le a_2 \mid \lnot b \mid b_1 \wedge b_2 \\ c &::= \mathtt{skip} \mid x := a \mid c_1 ; c_2 \mid \mathtt{if}\ b\ \mathtt{then}\ c_1\ \mathtt{else}\ c_2 \mid \mathtt{while}\ b\ \mathtt{do}\ c \mid \mathtt{call}\ m \end{aligned}

式の値 ⟦a⟧σ∈Z\llbracket a \rrbracket\sigma \in \mathbb{Z}、⟦b⟧σ∈{tt,ff}\llbracket b \rrbracket\sigma \in \{\mathrm{tt}, \mathrm{ff}\} を、式の構造についての再帰で定める。⟦n⟧σ=n\llbracket n \rrbracket\sigma = n、⟦x⟧σ=σ(x)\llbracket x \rrbracket\sigma = \sigma(x)、⟦a1+a2⟧σ=⟦a1⟧σ+⟦a2⟧σ\llbracket a_1 + a_2 \rrbracket\sigma = \llbracket a_1 \rrbracket\sigma + \llbracket a_2 \rrbracket\sigma（−-、×\times も同様）、⟦a1÷k⟧σ=⌊⟦a1⟧σ/k⌋\llbracket a_1 \div k \rrbracket\sigma = \lfloor \llbracket a_1 \rrbracket\sigma / k \rfloor。⟦true⟧σ=tt\llbracket \mathtt{true} \rrbracket\sigma = \mathrm{tt}、⟦a1=a2⟧σ=tt\llbracket a_1 = a_2 \rrbracket\sigma = \mathrm{tt} となるのは ⟦a1⟧σ=⟦a2⟧σ\llbracket a_1 \rrbracket\sigma = \llbracket a_2 \rrbracket\sigma のとき（≤\le も同様）、¬\lnot と ∧\wedge は真理値の否定と連言。ブール式 bb を表明 {σ∣⟦b⟧σ=tt}\{\sigma \mid \llbracket b \rrbracket\sigma = \mathrm{tt}\} と同一視する。a1<a2a_1 \lt a_2 は ¬(a2≤a1)\lnot(a_2 \le a_1) の略記とする。

解釈 M\mathcal{M} とは、各操作名 m∈Opm \in \mathrm{Op} に関係 M(m)⊆Σ×Σ\mathcal{M}(m) \subseteq \Sigma \times \Sigma を割り当てるものをいう。解釈 M\mathcal{M} のもとでの実行関係 ⟨c,σ⟩⇓σ′\langle c, \sigma \rangle \Downarrow \sigma' を、次の規則で生成される最小の関係とする。

(Skip)⟨skip,σ⟩⇓σ(Assign)⟨x:=a,σ⟩⇓σ[x↦⟦a⟧σ](Seq)⟨c1,σ⟩⇓σ1⟨c2,σ1⟩⇓σ′⟨c1;c2,σ⟩⇓σ′(Call)(σ,σ′)∈M(m)⟨call m,σ⟩⇓σ′(IfT)⟦b⟧σ=tt⟨c1,σ⟩⇓σ′⟨if b then c1 else c2,σ⟩⇓σ′(IfF)⟦b⟧σ=ff⟨c2,σ⟩⇓σ′⟨if b then c1 else c2,σ⟩⇓σ′(WhF)⟦b⟧σ=ff⟨while b do c,σ⟩⇓σ(WhT)⟦b⟧σ=tt⟨c,σ⟩⇓σ1⟨while b do c,σ1⟩⇓σ′⟨while b do c,σ⟩⇓σ′\begin{aligned} &\text{(Skip)} && \langle \mathtt{skip}, \sigma \rangle \Downarrow \sigma \qquad\qquad \text{(Assign)} \quad \langle x := a, \sigma \rangle \Downarrow \sigma[x \mapsto \llbracket a \rrbracket\sigma] \\[4pt] &\text{(Seq)} && \frac{\langle c_1, \sigma \rangle \Downarrow \sigma_1 \qquad \langle c_2, \sigma_1 \rangle \Downarrow \sigma'}{\langle c_1 ; c_2, \sigma \rangle \Downarrow \sigma'} \qquad\qquad \text{(Call)} \quad \frac{(\sigma, \sigma') \in \mathcal{M}(m)}{\langle \mathtt{call}\ m, \sigma \rangle \Downarrow \sigma'} \\[4pt] &\text{(IfT)} && \frac{\llbracket b \rrbracket\sigma = \mathrm{tt} \qquad \langle c_1, \sigma \rangle \Downarrow \sigma'}{\langle \mathtt{if}\ b\ \mathtt{then}\ c_1\ \mathtt{else}\ c_2, \sigma \rangle \Downarrow \sigma'} \qquad \text{(IfF)} \quad \frac{\llbracket b \rrbracket\sigma = \mathrm{ff} \qquad \langle c_2, \sigma \rangle \Downarrow \sigma'}{\langle \mathtt{if}\ b\ \mathtt{then}\ c_1\ \mathtt{else}\ c_2, \sigma \rangle \Downarrow \sigma'} \\[4pt] &\text{(WhF)} && \frac{\llbracket b \rrbracket\sigma = \mathrm{ff}}{\langle \mathtt{while}\ b\ \mathtt{do}\ c, \sigma \rangle \Downarrow \sigma} \qquad\qquad \text{(WhT)} \quad \frac{\llbracket b \rrbracket\sigma = \mathrm{tt} \qquad \langle c, \sigma \rangle \Downarrow \sigma_1 \qquad \langle \mathtt{while}\ b\ \mathtt{do}\ c, \sigma_1 \rangle \Downarrow \sigma'}{\langle \mathtt{while}\ b\ \mathtt{do}\ c, \sigma \rangle \Downarrow \sigma'} \end{aligned}

⟨c,σ⟩⇓σ′\langle c, \sigma \rangle \Downarrow \sigma' となる σ′\sigma' が存在するとき、cc は σ\sigma から停止するという。

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

閉包の状態

定義

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

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

これを使っている定理

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