Coqで分離論理(separation logic) - keigoiの日記

分離論理は、ヒープ領域に関する論理結合子をもつ論理体系だ。ホーア論理の拡張であり、ヒープを使うプログラムの仕様を書いたり検証したりといったことに使える。 具体的には、 A ∧ B (AかつB) によく似た、 A ** B という論理結合子が追加されている。これは Aで言及しているポインタと、 Bで言及しているポインタが指しているヒープ領域が、分離されている(≒エイリアシングがない)ことをいっている。 Affeldtさんが、Coqで分離論理を書いて、しかもそれを公開してくださっている。 http://staff.aist.go.jp/reynald.affeldt/seplog/ C言語で書かれたOSのヒープマネージャや、SmartMIPSのアセンブラで書かれた暗号プリミティブの検証をCoqでやっている。 こういったことを自分でも触れるようになりたいので、ICFEM2006のソースを写経して