分離論理 - mrsekut-p

分離論理

separation logic

分離論理はヒープ領域に関する論理結合子をもつ論理体系だ。ホーア論理の拡張であり、ヒープを使うプログラムの仕様を書いたり検証したりといったことに使える。

せっかくなので自分の理解も兼ねて説明してみる。

分離論理はホーア論理の基礎論理を直観主義論理(または古典論理または)から房論理(bunched logic; 訳語未定?)に変更したもの。

房論理は線形論理のようなリソース論理の仲間だが、直観主義論理(または古典論理)がそのまま埋め込まれているという特徴を持つ。具体的に言うと房論理の結合子は∧, ∨, →, ✱, -∗の5種類だが、最初の3つがそのまま直観主義論理。

分離論理では房論理の命題を、「メモリ権限が満たすべき条件」の記述に使う。たとえば、 M ⊨ P✱Q は「メモリ権限 M は命題 P✱Q を満たす」ことで、これは「権限M を独立した2つの権限M1, M2 に分割して、 M1 ⊨ P と M2 ⊨ Q が成り立つようにできる」ということを意味する。

これによりポインタの排他性を記述できる。たとえば、「値xは連結リストのポインタである」という性質を

IsList(x) := IsNil(x) ∨ (IsInt(deref(x)) ∧ IsList(deref(x + 1)))

と書くと途中で出現するポインタ同士の排他性が不明だが、

IsList(x) := IsNil(x) ∨ ((Has(x) ∧ IsInt(deref(x))) ✱ (Has(x + 1) ∧ IsList(deref(x + 1))))

と書けば、xが間接的に指すメモリを所有していることや、それらの全てのポインタが排他的であることが含意される。 (M ⊨ IsList(x) は M = { xを辿ったときに出てくる全てのメモリ領域 } としたときにのみ成立する)

...