--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/4.tex	Sat Mar 28 16:26:43 2009 +0900
@@ -0,0 +1,68 @@
+\section{ Protocol の正しさ}
+
+Merge Protocol の正しさの証明は、Protocol自体の正しさと、
+Protocolの実装を含めた正しさの二種類の正しさを示す必要がある。
+
+ここでは、(A)のProtocolの正しさを示す。Editor $0..n$ が、
+それぞれ、編集コマンド$C_{ij}$ (Editor $i$の$j$番目のコマンド,$j$は0から)を
+入力したとする。このコマンドは、Session ring を巡回する。
+巡回するたびに、各Editor $k$が{\tt NOP} Command $N_{kx}$を、その
+コマンドの前に付加する。
+% (A)では自分が既にCommandを送っていれば{\tt NOP}を付加する必要は
+% ないが、ここでは、必ず付加することにする。
+$x$は、コマンドの順序である。
+% $C_{ij}$の$j$は、{\tt NOP}を含めた番号に付け換える。
+
+Editor $m$では、
+\[  C_{m0} C_{x0} N_{00} .... N_{yz} \]
+などのコマンド列が実行されることになる。これを$C/N$の
+区別のないコマンド記号($E_{ij}$)で置き換えよう。
+\[  E_{m0} E_{x0} E_{00} .... E_{yz} \]
+NOPの付加手順から、
+他のEditorが送ったCommandには、その前の他のEditorからのCommandを
+受け取った後の、
+自分が送ったCommand(0以上の複数個)
+または、{\tt NOP}
+が必ず対応している。
+対応するCommandとは、Session ring 上で同時に実行されたと考えられる
+Command の集合と考えて良い。
+Command はSession ring  を一周するので、すべての
+Editor が同じCommandの集合を受け取っている。
+
+ここで、対応したCommandの集まり毎に列を分割し、
+Editor iの
+その集まりを集合と
+みなし$S_{ij}$ とする。この集合の列を$Z_i$とする。
+\[  Z_i = S_{i0} S_{i1} .... S_{in} \]
+定義から隣同士の$S_{ij}$には、
+対応したCommandが含まれることはない。
+
+この集合列$Z$は、すべてのEditorで同一となる。
+[証明]
+Editor $i$とEditor $j$で、$S_{ik}$と、$j$の$S_{jk}$が異なっている
+としよう。あるCommand $E_s$があって、
+$E_s \in S_{ik}$であって$E_s \in S_{jk}$でない。
+しかし、$E_s$
+はsession ringを一周しているので、$S_{ik}$と$S_{jk}$の両方に
+含まれているか、隣同士にあるはずである。両方に含まれていると
+すると仮定と矛盾するので、隣同士になるはずである。しかし、隣同士で
+あれば、Command の分割の方法に矛盾する。[証明終り]
+
+従って、$S_i$をEditor idとCommand順序によってソートしてやれば、
+すべてのEditorで、同一なCommand列を得ることが出来る。
+ソートのタイミングは、対応するコマンドがすべて自分に到着した時点である。
+自分の送った新しいコマンド、または、新しい{\tt NOP}が
+来たことによって、その一つ前までが対応しているものだということがわかる
+ので、その時点でソートしてやれば良い。従って、Merge Protocolにより、
+すべてのEditorで同一の編集結果が得られることがわかった。
+
+(B)では、{\tt NOP}の挿入の代わりに{\tt ack}を、もう一周させている。
+{\tt ack} が来た時点で、対応するCommandの集合が確定する。あるいは、
+仮想的に{\tt NOP}を挿入したと考えると、その{\tt NOP}は、{\tt ack}
+の前に挿入されていると考えて良い。従って、(A)と同じように集合列$Z$
+を、すべてのEditorで同一となるように決めることが出来る。
+
+プロトコルの実装の正しさは、実装言語であるJavaに深く依存するので、
+このように簡単に証明することは出来ない。そこで、
+モデル検査器であるJava PathFinder\cite{havelund98model}を用いる。
+