分離論理
separation logic
狀態は store と heap の組$ (s,h)
store$ sは變數を値に對應させる函數。大體のところ stack 領域に當たる
表現$ eを store$ sで評價した結果を$ \llbracket e\rrbracket_sと書く
heap$ hは memory 番地を値に對應させる部分函數。大體のところ heap 領域に當たる
heap$ hと$ h'はその定義域 (domain) が重ならない時、互ひに素 (disjoint) であると言ひ$ h\bot h'と書く
狀態$ (s,h)で assertion$ Pが成り立つならば$ s,h\vDash Pと書く assertion$ \bf emp。heap$ hが全ての memory 番地で未定義ならば$ s,h\vDash{\bf emp} memory 番地と値との二項關係$ e\mapsto e'。$ h(\llbracket e\rrbracket_s)=\llbracket e'\rrbracket_sであり$ \llbracket e\rrbracket_s以外の memory 番地では未定義であるならば$ s,h\vDash e\mapsto e' assertion の二項演算子$ P*Q(star。分離連言 (separating conjunction))。heap を互ひに素な二部分に分割できる。heap$ hに對して、$ h=h_1\cup h_2且つ$ h_1\bot h_2且つ$ s,h_1\vDash P且つ$ s,h_2\vDash Qである$ h_1,h_2が存在するならば$ s,h\vDash P*Q assertion の二項演算子$ P-\negthickspace*Q(magic wand。分離含意 (separating implication))。heap$ hに對して、$ h'\bot h且つ$ s,h'\vDash Pである heap$ h'が必ず$ s,h\cup h'\vDash Qでもあるならば$ s,h\vDash P-\negthickspace*Q assertion の二項演算子$ P\mathrlap{*}{\cup}Q(sepish。重複連言 (overlapping conjunction))。$ s,h_P\vDash P且つ$ s,h_Q\vDash Qであり交はり$ h_P\cap h_Qが空集合でないかもしれないならば、$ s,h_P\cup h_Q\vDash P\mathrlap{*}{\cup}Q modus ponens$ \frac{s,h\vDash P*(P-\negthickspace*Q)}{s,h\vDash Q} frame rule$ \frac{\{P\}C\{Q\}}{\{P*R\}C\{Q*R\}}{\rm mod}(C)\cap{\rm fv}(R)=\varnothing
$ {\rm mod}(C)は處理$ Cの變更 (modify) する變數の集合 concurrent separation logic (CSL)
$ \frac{\{P_1\}C_1\{Q_1\}\quad\{P_2\}C_2\{Q_2\}}{\{P_1*P_2\}C_1||C_2\{Q_1*Q_2\}}.