分離論理
概要
分離論理（separation logic）とは、記憶領域（ヒープ）を書き換えるプログラムの正しさを述べて証明するために Hoare 論理を拡張した論理である。論理式の真偽を変数の値とヒープの組で定め、ヒープを交わらない 2 つの部分に分けてそれぞれで $P$ と $Q$ が成り立つという分離連言 $P\ast Q$ と、それと随伴する分離含意をもつ。プログラムは持っていない番地に触れたときだけ誤りを起こし、割り当てには未使用の番地を選ぶという局所性をもつ。この局所性から、命令が触れない部分 $R$ を事前・事後条件に $\ast R$ で付け加えてよいという frame 規則が健全であることが従う。
分離論理（separation logic）は、記憶領域（ヒープ）を書き換えるプログラムの正しさを述べて証明するための論理である。論理式の真偽を「変数の値」と「ヒープ」の組で定め、通常の論理結合子に加えて、ヒープを交わらない 2 つの部分に分けてそれぞれで $P$ と $Q$ が成り立つという 分離連言 $P\ast Q$ と、それと随伴する 分離含意 $P\mathbin{-\!\!\ast}Q$ をもつ。J. C. Reynolds、P. W. O'Hearn、S. Ishtiaq らが 2000 年前後に Hoare 論理を拡張して作った（Rey02 §1）。
分離論理の中心は frame 規則
$$
\frac{\{P\}\,c\,\{Q\}}{\{P\ast R\}\,c\,\{Q\ast R\}}\qquad(c\text{ が書き換える変数は }R\text{ に自由に現れない})
$$
である。プログラムが実際に触れる記憶だけについて述べた仕様から、触れない部分 $R$ が変わらないことが自動的に従う。この記事では、ヒープのモデルと論理式の意味を定め、分離連言と分離含意の随伴を示したうえで、小さなプログラム言語の意味論を記憶の誤りまで含めて定め、プログラムの局所性を証明し、そこから frame 規則の健全性を導く。
ヒープのモデル
整数の全体を $\mathbb Z$ とし、正の整数を 番地 とよぶ（$0$ は番地でなく、空のポインタ nil に使う）。
- 変数の集合 $\mathrm{Var}$ から $\mathbb Z$ への写像を ストア という。
- 番地の有限集合を定義域とし $\mathbb Z$ に値をとる部分関数を ヒープ という。定義域が空のヒープを $\emptyset$ と書く。
- ヒープ $h_0,h_1$ の定義域が交わらないとき $h_0\perp h_1$ と書き、そのときに限り和 $h_0\uplus h_1$（両方の定義域の上で $h_0,h_1$ に一致するヒープ）を考える。
$\uplus$ は可換かつ結合的で、$\emptyset$ が単位元であり、$h_0\uplus h_1=h_0\uplus h_1'$ なら $h_1=h_1'$ である。式 $e$（変数と整数から $+,-,\times$ で作る項）の値 $[\![e]\!]s$ はストア $s$ だけで決まり、ヒープに依存しない。
論理式は、式の等号・大小、$\mathbf{emp}$、$e\mapsto e'$ から、$\land,\lor,\lnot,\to$、量化子 $\exists x,\forall x$（$x$ は整数を動く）、$\ast$、$\mathbin{-\!\!\ast}$ で組み立てる。ストア $s$ とヒープ $h$ での成立 $s,h\models P$ を次で定める。式の等号・大小はヒープによらず通常どおり、$\land,\lor,\lnot,\to$ と量化子も通常どおりとする。
- $s,h\models\mathbf{emp}$ $\iff$ $h=\emptyset$。
- $s,h\models e\mapsto e'$ $\iff$ $h$ の定義域が $\{[\![e]\!]s\}$ で、$h([\![e]\!]s)=[\![e']\!]s$。
- $s,h\models P\ast Q$ $\iff$ $h=h_0\uplus h_1$、$s,h_0\models P$、$s,h_1\models Q$ となる $h_0\perp h_1$ がある。
- $s,h\models P\mathbin{-\!\!\ast}Q$ $\iff$ $h'\perp h$ かつ $s,h'\models P$ となるすべての $h'$ について $s,h\uplus h'\models Q$。
すべての $s,h$ で成り立つ論理式を 妥当 といい、$P\to Q$ が妥当であることを $P\models Q$ と書く。$e\mapsto-$ は $\exists v.\,e\mapsto v$（$v$ は $e$ に現れない）の略記である。
Rey02 §2–§3 の定義に沿う（そこではストアを有限個の変数の上で考え、番地の集合を整数の無限部分集合としている）。$e\mapsto e'$ はヒープがちょうど 1 つの番地からなることを要求する。ヒープの他の部分について何も言わないためには $(e\mapsto e')\ast\mathbf{true}$ と書く。論理式の成立は、ストアについては自由変数の値だけで決まる（論理式の組み立てに関する帰納法）。
分離連言と分離含意
- $P\ast Q$ と $Q\ast P$、$(P\ast Q)\ast R$ と $P\ast(Q\ast R)$、$P\ast\mathbf{emp}$ と $P$ は、それぞれ同じ $s,h$ で成り立つ。
- $P\models P'$、$Q\models Q'$ なら $P\ast Q\models P'\ast Q'$。
- $P\ast Q\models R$ であることと $P\models Q\mathbin{-\!\!\ast}R$ であることは同値である。
1 と 2 は $\uplus$ の可換性・結合性・単位元と定義から直ちに従う。3 を示す。$P\ast Q\models R$ とし、$s,h\models P$ とする。$h'\perp h$、$s,h'\models Q$ なら、分け方 $h\uplus h'$ により $s,h\uplus h'\models P\ast Q$、よって $s,h\uplus h'\models R$ である。したがって $s,h\models Q\mathbin{-\!\!\ast}R$。逆に $P\models Q\mathbin{-\!\!\ast}R$ とし、$s,h\models P\ast Q$ とする。$h=h_0\uplus h_1$、$s,h_0\models P$、$s,h_1\models Q$ と分けると $s,h_0\models Q\mathbin{-\!\!\ast}R$ なので、$h_1$ を加えて $s,h\models R$ である。$\square$
3 は、ヒープ全体が $\uplus$ について部分的な可換モノイドをなすことから来る、Heyting代数 の $\land$ と $\to$ の随伴と同じ形の関係である。分離論理の論理式は、通常の結合子と $\ast,\mathbin{-\!\!\ast}$ を併せもつ「bunched implications の論理」のモデルになっている（Rey02 §1・§3）。
$s(x)=5$ とし、$h_1:=\{5\mapsto1\}$ とする。$s,h_1\models x\mapsto1$ だが、$h_1$ を交わらない 2 つに分けると一方は空なので $s,h_1\not\models(x\mapsto1)\ast(x\mapsto1)$ である。よって $P\models P\ast P$ は一般に成り立たない（縮約の不成立）。また $s(y)=6$、$h_2:=\{6\mapsto2\}$ とすると $s,h_1\uplus h_2\models(x\mapsto1)\ast(y\mapsto2)$ だが $s,h_1\uplus h_2\not\models x\mapsto1$ である。よって $P\ast Q\models P$ も成り立たない（弱化の不成立）。この意味で分離論理の $\ast$ は 線形論理 の乗法的連言に似た部分構造的な結合子である。
$(x\mapsto-)\ast(y\mapsto-)\models x\ne y$ である。実際、$h=h_0\uplus h_1$ で $h_0$ の定義域が $\{s(x)\}$、$h_1$ の定義域が $\{s(y)\}$ なら、$h_0\perp h_1$ から $s(x)\ne s(y)$ である。通常の連言 $(x\mapsto-)\land(y\mapsto-)$ はヒープが 1 つの番地だけからなることを言うので、逆に $x=y$ を導く。
プログラムと Hoare 三つ組
プログラムを
$$
c::=\mathbf{skip}\mid x:=e\mid x:=[e]\mid [e]:=e'\mid x:=\mathbf{cons}(e)\mid\mathbf{dispose}(e)\mid c_1;c_2\mid\mathbf{if}\ b\ \mathbf{then}\ c_1\ \mathbf{else}\ c_2\mid\mathbf{while}\ b\ \mathbf{do}\ c
$$
で定める（$b$ は式の等号・大小を $\land,\lnot$ で組んだ条件）。$[e]$ は番地 $[\![e]\!]s$ の中身を表す。実行の関係 $\langle c,s,h\rangle\Downarrow\tau$（$\tau$ は状態 $(s',h')$ か記憶の誤り $\mathsf{err}$）を、次の規則で生成される最小の関係とする。$\ell:=[\![e]\!]s$、$s[x\mapsto n]$ は $x$ の値だけを $n$ に替えたストアとする。
- $\mathbf{skip}$ は $(s,h)$ に、$x:=e$ は $(s[x\mapsto[\![e]\!]s],h)$ に進む。
- $\ell\in\operatorname{dom}h$ のとき、$x:=[e]$ は $(s[x\mapsto h(\ell)],h)$ に、$[e]:=e'$ は $\ell$ での値だけを $[\![e']\!]s$ に替えたヒープへ、$\mathbf{dispose}(e)$ は $h$ を $\operatorname{dom}h\setminus\{\ell\}$ に制限したヒープへ進む。$\ell\notin\operatorname{dom}h$ のとき、この 3 つは $\mathsf{err}$ に進む。
- $x:=\mathbf{cons}(e)$ は、$\operatorname{dom}h$ に属さない任意の番地 $m$ について $(s[x\mapsto m],\,h\uplus\{m\mapsto[\![e]\!]s\})$ に進む。
- $c_1;c_2$ は、$\langle c_1,s,h\rangle\Downarrow\mathsf{err}$ なら $\mathsf{err}$ に、$\langle c_1,s,h\rangle\Downarrow(s_1,h_1)$ かつ $\langle c_2,s_1,h_1\rangle\Downarrow\tau$ なら $\tau$ に進む。
- $\mathbf{if}$ は $b$ の真偽で $c_1$ か $c_2$ と同じに進む。$\mathbf{while}\ b\ \mathbf{do}\ c$ は、$b$ が偽なら $(s,h)$ に、真なら $c;\,\mathbf{while}\ b\ \mathbf{do}\ c$ と同じに進む。
$x:=e$、$x:=[e]$、$x:=\mathbf{cons}(e)$ の左辺に現れる変数の全体を $\operatorname{mod}(c)$ と書く。
Rey02 §2 の言語から 1 番地ずつの割り当てに簡単にし、遷移を 1 歩ずつ追う代わりに最終結果だけを定めたものである。割り当てる番地の選び方は決まっていない。止まらない実行は $\Downarrow$ のどの $\tau$ にも対応しない。規則に関する帰納法で、$\langle c,s,h\rangle\Downarrow(s',h')$ なら $\operatorname{mod}(c)$ に属さない変数の値は $s$ と $s'$ で等しい。
$\{P\}\,c\,\{Q\}$ が 妥当 であるとは、$s,h\models P$ となるすべての $s,h$ について、$\langle c,s,h\rangle\Downarrow\mathsf{err}$ とならず、$\langle c,s,h\rangle\Downarrow(s',h')$ ならば $s',h'\models Q$ であることをいう。
これは部分正当性（止まれば正しい）の仕様だが、記憶の誤りを起こさないことは要求する（Rey02 §4）。「仕様を満たすプログラムは解放済みの番地や割り当てていない番地に触れない」ことが仕様に含まれる。
局所性と frame 規則
$h=h_0\uplus h_1$ とする。任意のプログラム $c$ とストア $s$ について次が成り立つ。
- （誤りの単調性）$\langle c,s,h\rangle\Downarrow\mathsf{err}$ ならば $\langle c,s,h_0\rangle\Downarrow\mathsf{err}$。
- （frame 性）$\langle c,s,h_0\rangle\Downarrow\mathsf{err}$ でなく、$\langle c,s,h\rangle\Downarrow(s',h')$ ならば、$h'=h_0'\uplus h_1$ かつ $\langle c,s,h_0\rangle\Downarrow(s',h_0')$ となるヒープ $h_0'$ がある。
$\langle c,s,h\rangle\Downarrow\tau$ の導出に関する帰納法で、すべての分け方 $h=h_0\uplus h_1$ について 1 と 2 を同時に示す。
基本の命令．$\mathbf{skip}$ と $x:=e$ はヒープを変えず誤りも起こさないので、$h_0'=h_0$ でよい。$x:=[e]$、$[e]:=e'$、$\mathbf{dispose}(e)$ は $\ell\notin\operatorname{dom}h$ のときだけ誤りになり、そのとき $\ell\notin\operatorname{dom}h_0$ なので 1 が成り立つ。2 の仮定のもとでは $\ell\in\operatorname{dom}h_0$ なので $h(\ell)=h_0(\ell)$ であり、$h$ の $\ell$ を読む・書き換える・取り除くことは $h_0$ の $\ell$ について同じことをして $h_1$ を加えることと同じである。$x:=\mathbf{cons}(e)$ は誤りを起こさない。$h$ から番地 $m\notin\operatorname{dom}h$ を選ぶ実行について、$m\notin\operatorname{dom}h_0$ なので同じ $m$ を選ぶ実行が $h_0$ からもあり、$m\notin\operatorname{dom}h_1$ から $h\uplus\{m\mapsto v\}=(h_0\uplus\{m\mapsto v\})\uplus h_1$ である。
合成 $c_1;c_2$．1：$\langle c_1,s,h\rangle\Downarrow\mathsf{err}$ なら、帰納法の仮定から $\langle c_1,s,h_0\rangle\Downarrow\mathsf{err}$ で、$c_1;c_2$ も $h_0$ から誤りになる。そうでなく $\langle c_1,s,h\rangle\Downarrow(s_1,h'')$、$\langle c_2,s_1,h''\rangle\Downarrow\mathsf{err}$ とする。$c_1$ が $h_0$ から誤りになれば終わる。ならなければ、$c_1$ についての 2 から $h''=h_0''\uplus h_1$、$\langle c_1,s,h_0\rangle\Downarrow(s_1,h_0'')$ となり、$c_2$ の導出と分け方 $h''=h_0''\uplus h_1$ についての 1 から $\langle c_2,s_1,h_0''\rangle\Downarrow\mathsf{err}$ なので、$c_1;c_2$ は $h_0$ から誤りになる。2：$c_1;c_2$ が $h_0$ から誤りにならないので、$c_1$ も $h_0$ から誤りにならず、上と同じく $h''=h_0''\uplus h_1$、$\langle c_1,s,h_0\rangle\Downarrow(s_1,h_0'')$ を得る。$\langle c_2,s_1,h_0''\rangle\Downarrow\mathsf{err}$ でもない（そうなら $c_1;c_2$ が $h_0$ から誤りになる）ので、$c_2$ についての 2 から $h'=h_0'\uplus h_1$、$\langle c_2,s_1,h_0''\rangle\Downarrow(s',h_0')$ となり、$\langle c_1;c_2,s,h_0\rangle\Downarrow(s',h_0')$ である。
$\mathbf{if}$ と $\mathbf{while}$．条件 $b$ の真偽はストアだけで決まるので、$h$ と $h_0$ から同じ規則が使われる。$\mathbf{if}$ では選ばれた $c_i$ の導出に、$\mathbf{while}$ の真の場合は前提 $\langle c;\,\mathbf{while}\ b\ \mathbf{do}\ c,\,s,h\rangle\Downarrow\tau$ の導出に帰納法の仮定を当て、同じ規則で戻せばよい。偽の場合は $\mathbf{skip}$ と同じである。$\square$
Rey02 §2 の末尾はこの性質を 1 歩ずつの遷移の言葉で述べている。証明の要点は、割り当てが「まだ使われていない番地」を選ぶことと、誤りが「持っていない番地に触れる」ことだけから起こることである。
$\{P\}\,c\,\{Q\}$ が妥当で、$\operatorname{mod}(c)$ のどの変数も $R$ に自由に現れないならば、$\{P\ast R\}\,c\,\{Q\ast R\}$ は妥当である。
$s,h\models P\ast R$ とし、$h=h_0\uplus h_1$、$s,h_0\models P$、$s,h_1\models R$ と分ける。$\{P\}c\{Q\}$ の妥当性から $\langle c,s,h_0\rangle\Downarrow\mathsf{err}$ ではない。thm-sl-locality の 1 の対偶から $\langle c,s,h\rangle\Downarrow\mathsf{err}$ でもない。$\langle c,s,h\rangle\Downarrow(s',h')$ とすると、thm-sl-locality の 2 から $h'=h_0'\uplus h_1$、$\langle c,s,h_0\rangle\Downarrow(s',h_0')$ であり、妥当性から $s',h_0'\models Q$ である。$s'$ と $s$ は $\operatorname{mod}(c)$ の外で一致し、$R$ の自由変数はその外にあるので、$s',h_1\models R$ である。よって $s',h'\models Q\ast R$。$\square$
Rey02 §4 はこの議論の概略を述べている。frame 規則は O'Hearn による（同 §4）。
局所公理と証明の例
次の三つ組は妥当である。
- $\{e\mapsto-\}\ [e]:=e'\ \{e\mapsto e'\}$
- $\{e\mapsto-\}\ \mathbf{dispose}(e)\ \{\mathbf{emp}\}$
- $\{\mathbf{emp}\}\ x:=\mathbf{cons}(e)\ \{x\mapsto e\}$（$x$ は $e$ に現れない）
- $\{e\mapsto v\}\ x:=[e]\ \{x=v\land e\mapsto v\}$（$x$ は $e,v$ に現れない）
証明を開く
1・2・4：前提から $\operatorname{dom}h=\{\ell\}$ なので誤りは起こらない。1 では結果のヒープは $\{\ell\mapsto[\![e']\!]s\}$、2 では $\emptyset$ である。4 では結果は $(s[x\mapsto h(\ell)],h)$ で $h(\ell)=[\![v]\!]s$、$x$ は $e,v$ に現れないので $e,v$ の値は変わらず、$x=v$ と $e\mapsto v$ が成り立つ。3：誤りは起こらず、結果は $(s[x\mapsto m],\{m\mapsto[\![e]\!]s\})$ で、$x$ は $e$ に現れないので $x\mapsto e$ が成り立つ。$\square$
これらは命令が触れる 1 番地だけを述べている。frame 規則を当てれば、例えば $\{(e\mapsto-)\ast R\}\,[e]:=e'\,\{(e\mapsto e')\ast R\}$ が任意の $R$ について得られる（$[e]:=e'$ は変数を書き換えない）。ほかに、Hoare 論理の合成規則（$\{P\}c_1\{R\}$ と $\{R\}c_2\{Q\}$ から $\{P\}c_1;c_2\{Q\}$）と帰結の規則（$P'\models P$、$\{P\}c\{Q\}$、$Q\models Q'$ から $\{P'\}c\{Q'\}$）も、妥当性の定義から直ちに妥当である。ヒープに依存しない論理式 $\pi$ について $(\pi\land P)\ast Q$ と $\pi\land(P\ast Q)$ は同じ $s,h$ で成り立つ。
$t,u$ を $x,y,a,b$ と異なる変数とすると、
$$
\{(x\mapsto a)\ast(y\mapsto b)\}\ \ t:=[x];\ u:=[y];\ [x]:=u;\ [y]:=t\ \ \{(x\mapsto b)\ast(y\mapsto a)\}
$$
は妥当である。各命令の局所公理に、その命令が触れない番地を frame 規則で付け加えていけばよい。
途中の論理式を開く
$t:=[x]$ に局所公理 4 と枠 $y\mapsto b$ を当てて $(t=a\land x\mapsto a)\ast(y\mapsto b)$ を得る。$u:=[y]$ に局所公理 4 と枠 $t=a\land x\mapsto a$（$u$ を含まない）を当てて $t=a\land u=b\land((x\mapsto a)\ast(y\mapsto b))$ を得る。これは $(x\mapsto-)\ast(t=a\land u=b\land y\mapsto b)$ を導くので、$[x]:=u$ に局所公理 1 と枠を当てて $(x\mapsto u)\ast(t=a\land u=b\land y\mapsto b)$、同様に $[y]:=t$ の後で $t=a\land u=b\land((x\mapsto u)\ast(y\mapsto t))$ を得る。帰結の規則でこれを $(x\mapsto b)\ast(y\mapsto a)$ に弱める。
事前条件の $\ast$ が $x\ne y$ を含意する（ex-sl-distinct）ことが、2 つの書き込みが互いに干渉しないことの根拠になっている。
反例：条件を外すと frame 規則は成り立たない
表の各行は、thm-sl-frame の 1 つの条件を外したときに妥当でなくなる三つ組を示す。
| 外す条件 | 反例 | 成り立たなくなること |
|---|---|---|
| $\ast$ を通常の連言 $\land$ に替える | $\{x\mapsto-\}[x]:=4\{x\mapsto4\}$ に $R=(y\mapsto3)$ を $\land$ で付ける | $\{x\mapsto-\land y\mapsto3\}[x]:=4\{x\mapsto4\land y\mapsto3\}$ の妥当性 |
| 書き換える変数が $R$ に現れないこと | $\{\mathbf{emp}\}\,x:=1\,\{\mathbf{emp}\}$ と $R=(x=0)$ | $\{\mathbf{emp}\ast x=0\}\,x:=1\,\{\mathbf{emp}\ast x=0\}$ の妥当性 |
| 妥当性に「誤りを起こさない」を含めること | 誤りを「結果なし」と数えると $\{\mathbf{emp}\}[x]:=7\{\mathbf{false}\}$ が妥当になる。$R=(x\mapsto3)$ | $\{x\mapsto3\}[x]:=7\{\mathbf{false}\}$ の妥当性 |
1 行目：事前条件はヒープが 1 番地からなり $x=y$ となることを言い、実行後は $y\mapsto4$ なので $y\mapsto3$ が偽になる（Rey02 §4 の例）。2 行目：事前条件 $x=0$ のもとで実行後は $x=1$ である。3 行目：$\mathbf{emp}$ のもとで $[x]:=7$ は必ず誤りになるので、誤りを結果に数えない定め方では事後条件 $\mathbf{false}$ でも妥当になってしまうが、$x\mapsto3$ のもとでは誤りなく止まる。frame 規則の健全性には、仕様が誤りを排除することが欠かせない。
関連項目
- 前提: 一階述語論理, 部分写像
- 比較: 線形論理, Heyting代数
- 発展: 循環証明体系(帰納的定義付き一階述語論理)
参考文献
Mathpediaは寄付と、参考文献の書籍リンク（Amazonアソシエイト）の紹介料で運営されています。 支援について ／ 寄付する
