セミナーの内容

プログラム検証の理論に基づいて，プログラムの正しさを数学的に証明するトレーニングをするセミナーです．

プログラム検証の理論を身につけると，プログラムの仕様記述，仕様の分析，コーディング，コードレビュー，テストといったプログラミング全般においてよい効果があると考えています．

このセミナーでは定理証明器を使用しません．その理由を説明します．定理証明器のよいポイントは3つあります．1つ目は証明の正しさをチェックしてくれる点，2つ目は証明の一部を人間の代わりに実行してくれる点，最後は証明の全体を構成して管理してくれる点です．応用においてはこれらの支援がとても役に立ちます．しかしその一方で，支援が強力であることから，理論や対象の理解が不十分であったとしても証明ができてしまうという問題もあります．

定理証明器に頼らず紙とペンを使って机上で証明することになると，証明のすべての詳細を自力で行う必要があります．証明の構成を考え，戦略を立て，どこまで証明できているか，何が残っているか，何が使えるのかを管理する必要があります．定理証明器の利点である証明のチェックがないので間違いを犯す可能性は高まりますが，その分，理論の理解を深め，証明の力を向上させることができると思います．特に構成力を高めることができると思います．定理証明器の上ではできる証明が，真っ白い紙の上では構成できないことを知れば，そこに訓練すべきことがあることがわかります．

プログラム

プログラム検証の理論を段階的に解説します．各段階で解説した部分に関する証明問題をやっていただきます。答え合わせのときには、証明の解説に参加していただきます。これが短時間で力をつけるよい方法だからです。

1. 最弱事前条件
2. 正当性の条件
3. 代入文
4. 条件文
5. ループ
6. 関数呼び出し

※　進捗に応じて，一部内容をスキップする場合があります．原則として，全問題を消化することよりも，確実な理解を優先します．

講師について

株式会社PRINCIPIA 代表取締役 初谷 久史

プロセス代数 CSP に基づいた検査ツール SyncStitch 開発者

国立情報学研究所トップエスイープロジェクト「モデル検査特論」講師

セミナー参加の前提条件

前提知識

• プログラミングの基礎知識
• 1階述語論理

必要なもの

• 計算用紙と筆記具、またはエディタ

Zoom URL

CONNPASS のメッセージにてお知らせします。

配布物

スライド資料を CONNPASS のメッセージで配布します．申し込まれるタイミングによっては，PayPal でお使いのメールアドレスに送付する場合もあります．メールが受信できることをご確認ください．

注意事項

• 配布資料の公開は禁止です．
• Zoom 上での表示名を CONNPASS のユーザ名と合わせていただけると助かります．荒しを防止するためです．

連絡先

ご質問等がありましたら isaac@principia-m.com までお気軽にご連絡ください．