静的検証ツールの分野で新たなタイプの製品が登場した。メモリー関連エラーの検出に特化した英Monoidics社の「Infer」だ。「Separation Logic」という近年開発されたソフトウエア科学の研究成果を活用している。従来の一般的な静的検証ツールよりも正確に、メモリーリークなどのメモリー関連エラーをチェックできるのが特徴だ。

 メモリーリーク検証ツールといえば、米IBM社の「Rational Purify」が著名だが、Purifyは静的検証ツールではなく、実際に対象となるソフトウエアを実行しながらメモリーリークを検出する動的検証ツールである。これに対し、静的検証によるメモリーリーク検出は、ソフトウエアを実行せずに、ソースコードの解析によって推定する。より上流工程で対処できるという利点がある。

 Monoidics社は、Separation Logicの発明者である英University College London教授のPeter O'Hearn氏らが2009年に設立した。来日したO'Hearn氏(同社 取締役)らにツールの特徴などについて聞いた。

(聞き手は進藤 智則=日経コンピュータ


Inferで用いている「Separation Logic」(分離論理)とはどのようなものか。

来日したMonoidics社 取締役兼共同創業者のPeter O'Hearn氏(左)、および同社CTO兼共同創業者のCristiano Calcagno氏(右)。Calcagno氏は、英Imperial College LondonのLecturerでもある。
来日したMonoidics社 取締役兼共同創業者のPeter O'Hearn氏(左)、および同社CTO兼共同創業者のCristiano Calcagno氏(右)。Calcagno氏は、英Imperial College LondonのLecturerでもある。

O'Hearn氏: Separation Logicは2000年ころ、Carnegie Mellon University教授のJohn Reynolds氏と私が共同で考案したものだ。

 我々はホーア論理(Hoare logic、Hoare Triple)がTony Hoare氏によって1960年代に提供されて以来、長年抱えている根元的な問題を長らく研究してきた。ホーア論理は多大な功績を残したが、ポインタを含む記述を扱えないという問題があった(関連記事)。そこで我々は、ホーア論理のような仕組みでポインタを扱えるよう、ホーア論理を拡張する研究を始めた。

事前条件/事後条件は、設計者が手動で記述するのか。

O'Hearn氏: 一般にホーア論理でいう事前条件/事後条件、および不変条件は、設計者が仕様として記述するものだが、我々のツールでは、これら事前/事後条件を自動的に推論し、生成することができる。ツールの使い手が事前/事後条件を記述したり、Separation Logicを理解したりする必要はない。

 我々のツールがコードをチェックする際、ツールはある意味、「科学者」のように振る舞う。「科学者のように振る舞う」というのは、ツールが仮説を持ってコードを解析するということだ。科学者が自然界を観察する際、仮説を持って望むようにだ。

 具体的には、我々のツールでは事前/事後条件を見つけ出すために、「Abduction(仮説的推論、仮説形成)」という技法を用いている。Abductionというのは、米国の哲学者Charles Peirce氏が100年以上も前の1870年代に考案したものだ。

 Abductionの研究は長らく停滞していたが、我々のツールでは、このAbductionの技法を自動化し、ツール内で利用できるようにした。ある仮説を生成し、その仮説の証明が失敗したら、別の仮説をトライする。科学者が自然界の法則について仮説を発見するような形だ。

トライアンドエラーのような側面があるということか。

O'Hearn氏: Abductionは、仮説生成のガイドの役割を果たす。ある仮説に基づく証明が失敗したら、それは次の仮説を生み出すガイトとなるからだ。確かにヒューリスティックな側面はあるが、単純なトライアンドエラーとは異なる。

 Abductionをソフトウエア検証で利用するには、二つのブレークスルーが必要だった。一つはAbductionをSeparation Logicと組み合わせること(関連論文)、もう一つはSeparation Logicのシンボリック実行だ(関連論文)。