SORが正しく動作する証明

問題の単純化・定式化

本プログラムは、以下のような構成を取っている。 ここでプログラムの実行はループごとに分離できるため、一回分のループが 正しく全てのインデックス範囲について実行されることを示す。
一回のループが回るということは、全ての断片のデータが更新可能になる、と読み替えることができる。 この条件は、初期状態から始まり、最終的に任意の要素に隣接するデータが、その要素が属する断片内に存在すればよい。

端のデータを交換する擬似コード

まず、記法の定義を行う。
(集合) ← (メソッドの種類, 引数) 
:メソッドを(集合)に対し呼び出す

S    : インデックス集合
D    : インデックス集合と、それに対応するデータ (map)
D.S  : Dに付随するインデックス集合
D[S0]: Dのうち、S0のインデックス範囲に相当するものを返す
adjacent(S) : Sの端に隣接するインデックス集合
edge(S)     : Sの端のインデックス集合

ここで、adjacent, edgeについては以下の性質を持つものとする。
∀Sa⊂S, adjcent(Sa)⊂ adjcent(S) ∪ S
これを元に、以下のコードを検証する。
class F{
  S : インデックス集合
  D : データ集合

  m_s(){
    adjacent(S) ← (m_r, D[edge(S)])
  }

  m_r(D_r){
    D += D_r
  }  

  split(){
    S → S0, S1
    D0 = D[S0 ∪ (adjacent(S0) ∩ D.S)]
    D1 = D[S1 ∪ (adjacent(S1) ∩ D.S)]
    S = S0; D = D0
    return S1, D1
  }

  merge(S0, D0){
    S += S0
    D += D0
  }
};

main(){
  各断片がSk, Dkを持ち、ΣSk == S_whole, Sk == Dk.S

  S_whole ← (m_s)
}

ここで、split(), merge()がメソッド実行の途中の任意のタイミングで呼ばれる。 また、一度呼ばれたRMI要求は必ず実行され、split()が行われると必ず対応するmerge()がいずれ呼ばれるものとする。
示すこと
最終的に
∀e∈S, adjacent(e) ⊂ D.S
Sの要素eについて、その上下左右の隣接要素は全てDに含まれる

証明

上記の証明すべき命題は、以下のように書き換えられる
(A) 途中のあらゆる遷移状態において、

 ∀e0, e1 | e1 ∈adjacent(e0) 
    ( S_whole中の隣接する要素の組e0, e1 )
 について、以下の三つのいずれかが成立する。

 (1): e1 ← (m_s)というRMIメッセージが存在
 (2): e0 ← (m_r, e1のデータ)というRMIメッセージが存在
 (3): e0 ∈ S, e1 ∈ D.S (となる断片が存在)

(B)上の1や2の状態は3に移行する
split()---merge()の遷移状態では、転送中の「断片」についてこれらの性質が成り立てばよいてする。
まず(A)を示す。
これにより、(A)が示された。

次に(B)だが、起こりうる状態遷移は で、(1)や(2)はメッセージを伴う状態でいずれかは次の状態に遷移するので、最終的に(3)に収束するとしてよい。
これらにより、証明すべき命題が示された。