プログラムの正しさを数学的に証明する形式検証への招待
セミナーの内容
プログラムの正しさを数学的に証明する技術を体験するセミナーです。プログラミングやテストに携わる人が対象です。基本的なプログラミングの知識だけで理解できる構成です。単に話を聞くだけでなく、手を動かして体験していただきます。数学を使う部分はほとんどツールがやってくれるので、数学の知識不足を心配する必要はありません。
数学を使う
オペレーティングシステムの研究やダイクストラ法で有名なダイクストラさんはいいました：「テストでバグがあることをは示せるが、バグがないことは証明できない！」
なぜ証明できないのでしょうか？ テストケースの数が多すぎて網羅できないからです。ではどうしたら証明できるのでしょうか？ ひとつの方法は数学を使うことです。数学は有限の記号と有限の手続きで無限を扱うことができるからです。
初等幾何学には「二等辺三角形の2つの底角は等しい」という有名な定理があります。二等辺三角形の種類は無限にあります。この定理は無限にあるどのような二等辺三角形でも2つの底角は等しいと主張しています。このような証明ができるのが数学の力です。底辺の長さが 10 cm のものだけとか、頂角の大きさが 10° の倍数のものだけとか、そういった制限はありません。
無限のバリエーションを持つ図形に対して証明ができる幾何学と同じように、プログラムの正しさを証明することができる理論があります。クイックソートの発明や並行システムの理論で有名なホーアさんが発明したホーア論理というものです。これを使うと無限にあるテストケースをすべてテストしたのと同等の結果を得ることができます。このセミナーで紹介するのはこの技術です。
数学の論文にも間違いがあることはありますし、ツールにバグがあることもあるでしょう。しかしそれでもテストと比較すれば圧倒的に高い精度でプログラムの正しさを確かめることができます。
証明技術を学ぶ意義
プログラムの正しさを証明する技術を学ぶと、加えて2つのよい効果が得られます。1つは仕様を明確にしたりテストの精度を高めたりする力がつく点です。証明というトレーニングで考える力や可能性に気づくセンスが鍛えられるからです。もう1つはプログラムがもっている性質を深く理解できるようになるという点です。直感的にしか理解していなかったプログラムの動きを数学的に分析できるようになると、正しさを支えているプログラムの性質に気づくようになります。このような経験と知識は普段のプログラミングにもよい効果を与えるでしょう。
プログラムが持つ性質を深く掘り下げる例として、このセミナーでは2分探索の証明をゴールにします。これは挑戦的なゴールです。2分探索は決して簡単なアルゴリズムではありません。事実、アルゴリズムの教科書には間違ったコードが載せられていたという話があります。このセミナーの最終段階では、理論とツールの力を使って2分探索を徹底的に研究します。
ツール
Isabelle という定理証明支援ツールを使います。ケプラー予想という数学の問題を証明するために使われたり、オペレーティングシステムの性質を検証するために使われたりと実績のあるツールです。
ツールの効果は3つあります。1つ目はもちろん証明そのものを支援してくれることです。現在のツールはとても賢くなっていて、かなりの証明を自動で行ってくれます。2つ目は証明のチェックです。十分な数学的訓練を積んだ人でも間違うことはあります。ツールは数学の規則を正しく使っているかすべてチェックしてくれるので誤りを防ぐことができます。最後の3つ目は証明の管理です。証明するプログラムが大きくなってくると、証明しなければならない項目も増えていきます。紙の上で証明していると証明しなければいけない項目を見落とすことがあります。ツールは何をどこまで証明したのか管理してくれるので、このような見落としをすることはありません。
プログラムの証明はツールと対話をするような感じで進みます。まず証明したいプログラムと仕様をツールに入れます。ツールに証明を指示すると「ここまでできました」と返ってきます。そのレポートを見て Isabelle にアドバイスを与えます。このように共同作業をして証明を完成させます。
プログラムが間違っていると証明できない結果が残ります。これを分析するとプログラムの間違いについての情報が得られます。それを元にプログラムを修正して、証明できるまで繰り返します。時に分析は難しくなることがありますが、それを乗り越えると力がつきます。
最高に楽しい知的ゲームへようこそ！
以下のような人にぜひ参加していただきたいと思います：
- プログラムをもっと深く理解したい人
- テストよりも高いレベルの品質保証を目指したい人
- 定理証明支援ツールとはどのようなものか知りたい人
- 2分探索を極めたい人
なによりもプログラムの正しさを証明すること自体が最高に面白いゲームです！ ぜひご参加ください。
プログラム
形式検証への招待
- 正当性：仕様とは何か？ プログラムが正しいとは？
- 数理論理学：なぜ数学を使うのか？
- 定理証明支援ツール Isabelle
- Isabelle による仕様分析
プログラムの正しさを数学的に証明するための理論
- 事前条件・事後条件
- 契約によるプログラミング
- Hoare 論理
Isabelle によるプログラムの正当性証明
- 条件文の証明：最大値・絶対値
- ループの証明：掛け算・べき乗
- 探索とは何か？：線型探索
- 2分法：自然数の平方根の近似値
- 2分探索
講師について
株式会社 PRINCIPIA 代表取締役 初谷 久史
CSP 理論に基づいたモデリング・検査ツール SyncStitch 開発者
国立情報学研究所トップエスイープロジェクト「並行システムの設計検証」講師
セミナー参加の前提条件
前提知識
必要な知識は変数、代入文、条件文、ループといった基本的なプログラミングの知識です。「～でない・かつ・または」といった高校で習う程度の論理の知識を仮定します。条件文やテストを書くときに使う範囲で十分です。
必要なもの
- 定理証明支援ツール Isabelle がインストールされた PC
使用するツール
以下のサイトからダウンロードできます。
配布物と Zoom meeting URL
セミナー開始時刻までにCONNPASS のメッセージにてお知らせします。
同じメッセージを複数回送信する場合があります。あらかじめご了承ください。
注意事項
- 配布資料の公開は禁止です。
- 不測の事態が生じセミナーを開催または完遂できなかった場合は、日を改めて再開催することで対処させていただきます。
- 都合により申し込み後に参加できなくなった場合は、同等のセミナーを再演する際にご参加いただけるよう配慮しますのでご連絡ください。
連絡先
ご質問等がありましたら isaac@principia-m.com までお気軽にご連絡ください。
画像で引用した文献
（参考文献ではありません）
- An Axiomatic Basis for Computer Programming, C. A. R. Hoare, 1969
- Textbook Errors in Binary Searching, Richard E. Pattis, 1988
- Introduction to the Theory of Programming Languages, Bertrand Meyer, 1990