かじもとにっき

ゆるふわなおはなしをかきます

Assertの話(2)

遅くなりましたが前回の続きです。
なお、Delphi Advent Calendar 2013 - Qiita十一日目の記事でもあります。

配列・レコード・代入

今回は\omegaによって代入を定義します。代入には単なる変数への代入だけでなく、変数が配列やレコード型の場合、その要素への代入も扱わなければなりません。
問題を出来るだけ単純に扱いたいので、配列とレコードを統一的に扱える数学的な枠組みを考えることにします。
まず、直積の定義を思い出しておきましょう。

定義

Iを添字域とする集合族A=\langle A_i;i\in I\rangleが与えられた時、A_iから\bigcup_{i\in I}A_iへの写像fで、各iに対してf(i)\in A_iとなるものの全体を、集合族Aの直積と言い、\prod_{i\in I}A_iと書く:
\prod_{i\in I}A_i=\{f:I\rightarrow\bigcup_{i\in I}A_i;\forall i\in I.f(i)\in A_i\}

そして、配列やレコードを直積の元と見なします。すなわち、配列を順序型を始域とする写像、レコードを識別子の集合を始域とする写像と考えるのです(配列の場合、上記の直積の定義で\forall i,j.A_i=A_jとなります)。そして、aが配列であるときa(i)a[i] 、レコードであるときa(i)a.iと書くことにします。

定義

配列やレコードが入れ子になっている場合を考えると、要素へのアクセスは、
a(i_1)(i_2)\cdots(i_n)のようになる。ここに現れる添字式の有限列、(i_1)(i_2)\cdots(i_n)を選択子と呼ぶ。特に、空の選択肢を\lambdaで表す。選択子の連結を\oplusで表すと、単純変数xx\oplus\lambdaとして扱うことが出来るので、変数はそれが単純変数であれ、配列やレコードと言った添字付き変数であれ、名前に選択子を付けた物として扱うことが出来る。

定理

s,t,uをそれぞれ選択子とすると、
s\oplus\lambda=\lambda\oplus s=s (単位元)
(s\oplus t)\oplus u = s\oplus(t\oplus u) (結合律)
がそれぞれ成り立つ。

定義

変数aの要素a\oplus seで置き換えた値をa(s;e)で表す。すなわち、a,bを同じ型の変数、saに適用可能な選択子としたとき、eを適切な型の式として、a(s;e)を次のように定義する:
a(\lambda;b) = b
a((i)\oplus s;e)(j)=\begin{cases}a(j)&(j\neq i)\\a(i)(s;e)&(j=i)\end{cases}

(0起点の)配列の配列a=\langle\langle 1,2,3\rangle,\langle 4,5,6\rangle\rangleに対し、
a([1][2];50)[0]=a[0]=\langle1,2,3\rangle
a([1][2];50)[1]=a[1]([2];50)=\langle 4,5,50\rangle

選択子s=(i)の長さが1 のとき、
a((i);e)(j)=\begin{cases}e&(j=i)\\a(j)&(j\neq i)\end{cases}

レコードb=\{\langle\text{'x'},1\rangle,\langle\text{'y'},2\rangle,\langle\text{'z'},3\rangle\}に対し、
b(x;100).x=100
b(x;100).y=2
b(x;100).y=3

これで代入を定義する準備が整いました。

定義

Eを式、\bf eを式の列、\bf xを名前の後ろに選択子が結合したものの列であるとする。このとき、字句置換R_{\bf e}^{\bf x}を次の規則で定める。
(1)\bf{x}=x_1,x_2,...,x_nが異なる名前の列(このとき、全ての選択子は\lambdaである)である時、R_{\bf e}^{\bf x}は式R中に現れる全ての自由変数x_iを、対応するe_iで置き換えた式を表す。
(2)abが異なる名前であるとき、
E^{\bf{x},a\oplus s,b\oplus t,\bf{y}}_{\bf{e},i,j,\bf{f}}=E^{\bf{x},b\oplus t,a\oplus s,\bf{y}}_{\bf{e},j,i,\bf{f}}
(3) 名前a\bf x のどの要素x_iの先頭にも現れない時、
E^{a\oplus s_1,a\oplus s_2,...,a\oplus s_n,\bf{x}}_{i_1,i_2,...,i_n,\bf{e}}=E^{a,\bf{x}}_{a(s_1;i_1)(s_2;i_2)\cdots(s_n;i_n),\bf{e}}

定義 代入

\bf eを式の列、\bf xを名前の後ろに選択子が結合したものの列であるとする。このとき、
\omega_{\bf{x}:=\bf{e}}P=P^{\bf{x}}_{\bf{e}}
(正確を期すと\bf eの各式が定義されるかの議論が必要であるが、簡単の為に今回は省略する)

この代入の定義はいわゆる多重代入を含んでおり、例えば\omega_{x,y:=y,x}(x>y)\Leftrightarrow y>xとなります。Delphiに多重代入は存在しませんが、プログラムを考える上では非常に便利な概念です。

選択文

定義

Pを述語、Sを文とした時、P\rightarrow Sをガード付き文と呼ぶ。SPが真の時のみ実行される。ガード付き文それ自体は文ではない。

定義

Gをガード付き文の有限集合とする。このとき、ifGを選択文と呼び、if\{B_1 \rightarrow S_1,B_2\rightarrow S_2,...,B_n\rightarrow S_n\}
の最弱事前条件を次のように定義する:
\omega_{ifG}P=(\exist_{1\leq i\leq n}i.B_i)\wedge(\forall_{1\leq i\leq n}i.B_i\Rightarrow\omega_{S_i}P)

ガードが一つも真でない場合、\omega_{ifG}P=\omega_{halt}Pなので、ifG の実行は放棄されます。ガードが1つ以上真ならば、その中から1つガード付き文B_i\rightarrow S_iを選び、文S_iを実行します。B_iが互いに排他的でない場合、ifGが非決定性を持ち込むことに注意して下さい。
条件が、選択文の最弱事前条件を含意することが分かれば十分であることがよくある
ので、次の定理が便利です。

定理

選択文ifG、述語Qに対し、
(1) Q\Rightarrow \exist_{1\leq i\leq n}i.B_i
(2) Q\wedge B_i \Rightarrow \omega_{S_i}P (1\leq i\leq nに対して)
が成り立つとき、また、その時に限りQ\Rightarrow\omega_{ifG}Pが成り立つ。

証明

(Q\Rightarrow\exist_{1\leq i\leq n}i.B_i)\wedge\forall_{1\leq i\leq n}i.Q\wedge B_i\Rightarrow\omega_{S_i}P
\Leftrightarrow(Q\Rightarrow\exist_{1\leq i\leq n}i.B_i)\wedge\forall_{1\leq i\leq n}i.Q\Rightarrow(B_i\Rightarrow\omega_{S_i}P)
\Leftrightarrow(Q\Rightarrow\exist_{1\leq i\leq n}i.B_i)\wedge(Q\Rightarrow\forall_{1\leq i\leq n}i.B_i\Rightarrow\omega_{S_i}P)
\Leftrightarrow Q\Rightarrow(\exist_{1\leq i\leq n}i.B_i)\wedge(\forall_{1\leq i\leq n}i.B_i\Rightarrow\omega_{S_i}P)
\Leftrightarrow Q\Rightarrow\omega_{ifG}P

簡単なプログラムの例

仕様\{true\}z:=?\{z=|x|\}を満たすプログラムを作ることを考えてみましょう。このプログラムで達成すべきことは事後条件に書かれています。すなわち、入力変数xの絶対値を出力変数zに求めろと言うことです。絶対値を求める関数はDelphiに存在しますが、今はそれを無視して自分で実装してみましょう。
事後条件を定義に戻すと、Q:z\geq 0\wedge(z=x\vee z=-x)となります。
そこで、Qを成り立たせる為の文を考えてみます。式内の左選言肢を見ると、z:=xとなっているので、z:=xが候補に挙がります。
では、どんな条件の下でz:=xを実行すればQが成り立つでしょうか。\omega_{z:=x}Qを計算すればそれが求まります。
\omega_{z:=x}Q\\\Leftrightarrow(z\geq 0\wedge(z=x\vee z=-x))^z_x\\\Leftrightarrow x\geq 0\wedge(x=x\vee x=-x)\\\Leftrightarrow x\geq 0
よって、x\geq 0の下でz:=xを実行すればQが成り立つことが分かりました。従って、次のプログラムが得られます:
if\{x\geq 0\rightarrow z:=x\}
さて、仕様で与えられた事前条件はtrueでした。つまり、どんな状態で開始してもQを満たして終了しなくてはなりません。しかし、上記のプログラムでは残念ながら、x<0の時、実行の放棄が起こってしまいます。実行放棄を起こさない為には、事前条件がガードの論理和を含意しなければなりません。
Q内の右選言肢を見ると、z:=-xもまたQを成り立たせる文の候補と考えられます。
z:=xの時と同様に、\omega_{z:=-x}Qを計算します。
\omega_{z:=-x}Q\\\Leftrightarrow(z\geq 0\wedge(z=x\vee z=-x))^z_{-x}\\\Leftrightarrow -x\geq 0\wedge(-x=x\vee -x=-x)\\\Leftrightarrow x\leq 0
つまり、x\leq 0の下でz:=-xを実行しても、Qが成り立ちます。
そして先のプログラムにこれを付け加えれば次のプログラムが得られます:
if\left\{ x\geq 0\rightarrow z:=x \\ x\leq 0\rightarrow z:=-x \right\}\\\{z\geq 0\wedge(z=x\vee z=-x)\}
このプログラムは条件文に関する定理に沿って作られましたので、証明は容易です。条件文が非決定性を持っていることにより、x=0の際にどちらの文を実行すべきかという決定を下す必要がなかったことに注意して下さい。
このプログラムをDelphiで実装すると、

if X >= 0 then Z := X else Z := -X;
Assert((Z >= 0) and ((Z = X) or (z = -X)))

のようになるでしょう(プログラムからは非決定性が除去されています)。

次回予告

次回は反復文について書く予定です。