イベントレポート：「ProofSummit2011」

作者 株式会社 豆蔵　小林 健一 投稿日 2011年10月5日

セクション

設計/アーキテクチャ,

デベロップメント

トピック

言語 ,

ソフトウェア検証 ,

プログラミング ,

形式手法

共有 |

定理証明支援系ツールとは

定理証明支援系ツールとは、コンピュータプログラムによって数学的定理の証 明を行うツールである。このツールは、数学の論理とプログラムの対応付けが発見されたことにより、プログラムの正しさを「証明する」という形で、ソフ トウェア開発においても利用することができる。代表的な定理証明支援系ツールには、Coq,Agda,Isabelle/HOL,ACL2などがある。

ソフトウェアの正しさを確認する手段としては、広くソフトウェアテストが行 われている。ソフトウェアテストと証明の大きな違いは、「仕様を正しく実装 していることを示すことができる」点である。ソフトウェアテストでは、欠陥 がないことは保証できない。証明を行うと、証明した内容については欠陥がな いことが保証される。証明による検証はテストと違い、網羅的な検証になって いる。

この定理証明支援系ツールは、関数型プログラミング言語を基礎としていることが多い。このため、現在の関数型プログラミング言語の流行に乗じて、にわかに注目を集めるようになってきた。

定理証明支援系ツールを扱う技術者勉強会としては、名古屋を中心とする ProofCafe (http://proofcafe.org/wiki/)が有名である。東京では、筆者と知人で主催するFormal Methods Forum(http://groups.google.com/group/fm-forum)が精力的に活動している。
2010年には名古屋にて、定理証明支援系ツールのイベント「Coq庵」が開催された(http://coq.g.hatena.ne.jp/keyword/Coq%E5%BA%B5)。

ProofSummit2011とは

上記のような盛り上がりの中、ICFP2011という関数型プログラミングに関する 国際会議、および併設ワークショップが9月18日から24日にかけて、東京で行われた(http://www.icfpconference.org/icfp2011/)
(http://www.icfpconference.org/affiliated.html)。

そこで、ProofCafeとFormal Methods Forumのメンバが中心となり、「Coq庵を、今年はICFPに合わせて東京で開催しよう」という意図で開催されたのが ProofSummit2011である。

開催の様子

参加者は総勢約50名という大人数で、会場はほぼ満員の盛況であった。

全体的な流れとして、まず午前中に定理証明支援系ツールCoq,Agdaのチュートリアルが行われた。@tmiya_氏によるCoq入門では、形式手法の概要から始まり、 Coqを使用しての簡単な証明のテクニックの解説が行われた。初心者向けの解説 に加え、証明しやすいプログラムの記述の仕方など、実践につながる解説まで が行われた。

@ikegami__氏によるAgda入門では、Agdaでのプログラミングの基礎から最新機能紹介まで幅広い解説が行われた。参加者からの質問も活発であった。

午後は、定理証明支援系ツールに関する応用トピックを解説するセッションが 3つ行われた。@mzp氏による「CoqによるMsgPackシリアライザの証明と実装」で は、MsgPackのモジュールの証明を行った事例が紹介された。証明済みのコードのパフォーマンスが、他の実装と比較して遅いことが課題として挙がっていた が、今後のパフォーマンス向上への挑戦が楽しみである。

次のセッションでは、@keigoi氏による「START SEPLOG COQ2」という題で、C言語のコードをCoqで証明する技法についての解説が行われた。C言語のような手続き型言語では破壊的代入が頻繁に行われるため、関数型言語のように簡単には証明が行えない。そこで、Separation Logicという公理系を使用し、Coqの中にC言語の簡易インタプリタを構築することで、証明を行う方法が紹介された。
Separation Logicを使った証明は、ここ数年の間に研究が盛り上がってきた分野である。

応用トピックセッションの最後は、@kikx氏による「ssreflect」の解説である。
ssreflectは、"small scale reflection"という、証明スタイルを実現するCoqの拡張ライブラリである。ssreflectを使用することで、Coqのコードがよりメ ンテナンスしやすくなる可能性がある。

3つのセッションのあとは、8人の方によるライトニングトークが行われた。 @masahiro_sakai氏による自動定理証明技術の紹介、@snisimu氏による、回路設計にAgdaを利用する話題等、一人5分では終わらない、濃い解説が印象的だった。

今後に向けて

ProofSummit2011は素晴らしい盛り上がりを見せたが、来年度の開催に向けて、 もう次の活動が始まっている。
興味のある方はぜひ、ProofCafeやFormal Methods Forumに参加していただきたい。

** 関連情報

※ ProofSummit2011 http://partake.in/events/ac41261d-6026-4d09-8814-5ad3e58446e8

※ Formal Methods Forum http://groups.google.com/group/fm-forum

※ ProofCafe http://proofcafe.org/wiki/