プログラムの正しさを数学的に証明する技術を体験するセミナーです。プログラミングやテストに携わる人が対象です。基本的なプログラミングの知識だけで理解できる構成です。単に話を聞くだけでなく、手を動かして体験していただきます。数学を使う部分はほとんどツールがやってくれるので、数学の知識不足を心配する必要はありません。
オペレーティングシステムの研究やダイクストラ法で有名なダイクストラさんはいいました：「テストでバグがあることをは示せるが、バグがないことは証明できない！」
なぜ証明できないのでしょうか？ テストケースの数が多すぎて網羅できないからです。ではどうしたら証明できるのでしょうか？ ひとつの方法は数学を使うことです。数学は有限の記号と有限の手続きで無限を扱うことができるからです。
初等幾何学には「二等辺三角形の2つの底角は等しい」という有名な定理があります。二等辺三角形の種類は無限にあります。この定理は無限にあるどのような二等辺三角形でも2つの底角は等しいと主張しています。このような証明ができるのが数学の力です。底辺の長さが 10 cm のものだけとか、頂角の大きさが 10° の倍数のものだけとか、そういった制限はありません。
無限のバリエーションを持つ図形に対して証明ができる幾何学と同じように、プログラムの正しさを証明することができる理論があります。クイックソートの発明や並行システムの理論で有名なホーアさんが発明したホーア論理というものです。これを使うと無限にあるテストケースをすべてテストしたのと同等の結果を得ることができます。このセミナーで紹介するのはこの技術です。
数学の論文にも間違いがあることはありますし、ツールにバグがあることもあるでしょう。しかしそれでもテストと比較すれば圧倒的に高い精度でプログラムの正しさを確かめることができます。
プログラムの正しさを証明する技術を学ぶと、加えて2つのよい効果が得られます。1つは仕様を明確にしたりテストの精度を高めたりする力がつく点です。証明というトレーニングで考える力や可能性に気づくセンスが鍛えられるからです。もう1つはプログラムがもっている性質を深く理解できるようになるという点です。直感的にしか理解していなかったプログラムの動きを数学的に分析できるようになると、正しさを支えているプログラムの性質に気づくようになります。このような経験と知識は普段のプログラミングにもよい効果を与えるでしょう。
プログラムが持つ性質を深く掘り下げる例として、このセミナーでは2分探索の証明をゴールにします。これは挑戦的なゴールです。2分探索は決して簡単なアルゴリズムではありません。事実、アルゴリズムの教科書には間違ったコードが載せられていたという話があります。このセミナーの最終段階では、理論とツールの力を使って2分探索を徹底的に研究します。
Isabelle という定理証明支援ツールを使います。ケプラー予想という数学の問題を証明するために使われたり、オペレーティングシステムの性質を検証するために使われたりと実績のあるツールです。
ツールの効果は3つあります。1つ目はもちろん証明そのものを支援してくれることです。現在のツールはとても賢くなっていて、かなりの証明を自動で行ってくれます。2つ目は証明のチェックです。十分な数学的訓練を積んだ人でも間違うことはあります。ツールは数学の規則を正しく使っているかすべてチェックしてくれるので誤りを防ぐことができます。最後の3つ目は証明の管理です。証明するプログラムが大きくなってくると、証明しなければならない項目も増えていきます。紙の上で証明していると証明しなければいけない項目を見落とすことがあります。ツールは何をどこまで証明したのか管理してくれるので、このような見落としをすることはありません。
プログラムの証明はツールと対話をするような感じで進みます。まず証明したいプログラムと仕様をツールに入れます。ツールに証明を指示すると「ここまでできました」と返ってきます。そのレポートを見て Isabelle にアドバイスを与えます。このように共同作業をして証明を完成させます。
プログラムが間違っていると証明できない結果が残ります。これを分析するとプログラムの間違いについての情報が得られます。それを元にプログラムを修正して、証明できるまで繰り返します。時に分析は難しくなることがありますが、それを乗り越えると力がつきます。
以下のような人にぜひ参加していただきたいと思います：
なによりもプログラムの正しさを証明すること自体が最高に面白いゲームです！ ぜひご参加ください。
必要な知識は変数、代入文、条件文、ループといった基本的なプログラミングの知識です。「～でない・かつ・または」といった高校で習う程度の論理の知識を仮定します。条件文やテストを書くときに使う範囲で十分です。
以下のサイトからダウンロードできます。