理工学部Faculty of Science and Engineering
COT400XE（計算基盤 / Computing technologies 400）プログラム検証論Plagram verification
真野 健Ken MANO
授業コードなどClass code etc
| 学部・研究科Faculty/Graduate school | 理工学部Faculty of Science and Engineering |
| 添付ファイル名Attached documents | |
| 年度Year | 2021 |
| 授業コードClass code | H6189 |
| 旧授業コードPrevious Class code | |
| 旧科目名Previous Class title | |
| 開講時期Term | 春学期授業/Spring |
| 曜日・時限Day/Period | 金3/Fri.3 |
| 科目種別Class Type | |
| キャンパスCampus | 小金井 |
| 教室名称Classroom name | |
| 配当年次Grade | |
| 単位数Credit(s) | |
| 備考（履修条件等）Notes | |
| 他学部公開科目Open Program | |
| 他学部公開（履修条件等）Open Program (Notes) | |
| グローバル・オープン科目Global Open Program | |
| 成績優秀者の他学部科目履修制度対象Interdepartmental class taking system for Academic Achievers | |
| 成績優秀者の他学部科目履修（履修条件等）Interdepartmental class taking system for Academic Achievers (Notes) | |
| 実務経験のある教員による授業科目Class taught by instructors with practical experience | |
| SDGsCPSDGs CP | |
| アーバンデザインCPUrban Design CP | |
| ダイバーシティCPDiversity CP | |
| 未来教室CPLearning for the Future CP | |
| カーボンニュートラルCPCarbon Neutral CP | |
| 千代田コンソ単位互換提供（他大学向け）Chiyoda Campus Consortium | |
| カテゴリー＜理工学部＞Category |
応用情報工学科 学科専門科目 |
すべて開くShow all
すべて閉じるHide All
Outline (in English)
Formal method is a promising approach for proving safety of software
systems rigorously and (partially) automatically using theorem
provers. Coq is one of the most popular theorem provers developed
mainly by INRIA. We study formal method using Coq.
授業で使用する言語Default language used in class
日本語 / Japanese
授業の概要と目的（何を学ぶか）Outline and objectives
ソフトウェアの安全性（バグやセキュリティホールがないこと）を，定理証明支援系と呼ばれる計算機ツールを用いて，厳密かつ（部分的に）機械的に証明する手法として，形式手法（数理的技法）に注目が集まっている．Coq は INRIA（フランス国立情報学自動制御研究所）を中心に開発されている代表的な定理証明支援系である．この Coq を用いた形式手法について学ぶ．
到達目標Goal
リストや自然数などを扱う簡単なプログラムを題材とし，その基本的な性質を Coq を用いて厳密に証明できる力を身につけることを目標とする．
この授業を履修することで学部等のディプロマポリシーに示されたどの能力を習得することができるか（該当授業科目と学位授与方針に明示された学習成果との関連）Which item of the diploma policy will be obtained by taking this class?
ディプロマポリシーのうち、「DP1」と「DP2」と「DP4」に関連
授業で使用する言語Default language used in class
日本語 / Japanese
授業の進め方と方法Method(s)（学期の途中で変更になる場合には、別途提示します。 /If the Method(s) is changed, we will announce the details of any changes. ）
進行状況にあわせて適宜進め方を変更するが，原則として，講義（Coq の理論的側面の解説）とそれに対応した演習（Coq を用いた実際の証明作成）とを織り交ぜて実施する．実習では，PC に Coq をインストールして用いる．
授業は Zoom を用いてオンラインで行う．詳細はおって学習支援システムに掲示する．
課題等に対するフィードバックは学習支援システムや授業などで行う．
アクティブラーニング（グループディスカッション、ディベート等）の実施Active learning in class (Group discussion, Debate.etc.)
なし / No
フィールドワーク（学外での実習等）の実施Fieldwork in class
なし / No
授業計画Schedule
※各回の授業形態は予定です。教員の指示に従ってください。
1：オリエンテーション
本授業のテーマおよび到達目標，概要と方法について述べる．
2：Coqでプログラミング
関数型プログラミング言語系としての Coq について解説する．
3：「型」＝「命題」, 「プログラム」＝「証明」
いわゆる Curry-Howard 同型対応（「型」と「命題」，「プログラム」と「証明」とをそれぞれ同一視する考え方）について解説する．
4：命題論理の証明(→)
含意→からなる命題論理式の証明を Coq を用いて作成する方法について解説する．
5：命題論理の証明(￢, ∨, ∧)
否定￢，論理和∨，論理積∧を含む命題論理式の証明を Coq を用いて作成する方法について解説する．
6：振り返り
中間レポート課題のフィードバックを行う．
7：リストの帰納的定義と証明(その一)
Coq の最大の特徴として強力な帰納的定義メカニズムを備えていることが挙げられる．基本的な型の例であるリスト型をとりあげ，その帰納的定義と Coq による証明作成について述べる．
8：リストの帰納的定義と証明(その二)
引き続き基本的な型の例であるリスト型をとりあげ，その帰納的定義と Coq による証明作成について述べる．リストを扱う簡単なプログラムを題材とし，その基本的な性質を Coq を用いて厳密に証明する．
9：自然数の帰納的定義と証明(その一)
リスト型と同様に基本的な自然数の型をとりあげ，その帰納的定義と Coq による証明作成について述べる．
10：自然数の帰納的定義と証明(その二)
引き続き自然数の型をとりあげ，その帰納的定義と Coq による証明作成について述べる．自然数を扱う簡単なプログラムを題材とし，その基本的な性質を Coq を用いて厳密に証明する．
11：自然数の帰納的定義と証明(その三)
引き続き自然数の型をとりあげ，その帰納的定義と Coq による証明作成について述べる．自然数やリストなどを複合的に扱うプログラムを題材とし，その基本的な性質を Coq を用いて厳密に証明する．
12：さまざまなタクティク
実際に証明を作成する上で有用となるさまざまなタクティクをいくつか紹介する．
13：証明駆動開発入門(その一)
本授業のハイライトとなる証明駆動開発について述べる．ソートを題材に，その仕様とプログラムを Coq で記述する．
14：証明駆動開発入門(その二)
引き続き証明駆動開発について述べる．実際にソートのプログラムが仕様をみたすことを Coq で証明し, Extraction して他言語のコードに変換する方法を学ぶ．
授業時間外の学習（準備学習・復習・宿題等）Work to be done outside of class (preparation, etc.)
【本授業の準備・復習等の授業時間外学習は、4時間を標準とする】指定する講義資料に事前に目を通し，講義終了後に復習することが望ましい．
テキスト（教科書）Textbooks
講義資料を配布する．
参考書References
★池渕未来: プログラミングCoq 〜絶対にバグのないプログラムの書き方〜.
https://www.iij-ii.co.jp/activities/programming-coq/
(本授業は全般にわたりこの優れたチュートリアルをベースにしています.)
★Software Foundations 日本語版 Wiki
http://www16.atwiki.jp/sf_j/pages/1.html
(米国ペンシルバニア大の Benjamin Pierce 教授のグループによって作成・公開されているドキュメントSoftware Foundationsの日本語版です.)
★Reynald Affeldt: 定理証明支援系Coq/SSReflect入門
https://staff.aist.go.jp/reynald.affeldt/ssrcoq/
(専門家によるモダンなCoq入門. Coqの拡張であるSSReflectの日本語による解説はたいへん貴重です.)
★The Coq Proof Assistant: A Tutorial.
http://coq.inria.fr/getting-started
(Coq の開発元からダウンロード可能な最も基本的なチュートリアルです.)
★Yves Bertot and Pierre Casteran: Interactive Theorem Proving and Program Development: Coq'Art. Springer (2004). ISBN: 3-540-20854-2
(本格的な洋書となりますが，参考書の定番です.)
成績評価の方法と基準Grading criteria
学期途中(50% 程度)と学期末(50% 程度)のレポート課題をもとに評価する．いずれも授業内容の応用である．電子メイルにより提出してもらう．
学生の意見等からの気づきChanges following student comments
先進的な新しいプログラミング言語をひとつマスターする感覚でCoqに接してもらえればと思います。証明はゲーム感覚で楽しんでください。たとえレポート課題が少々難しくても、自分自身で考え、手を動かしてみることが重要です。
学生が準備すべき機器他Equipment student needs to prepare
PC に Coq（バージョン 8.9 以降）をインストールして使用する．貸与 PC には既に Coq（に CoqIDE と呼ばれるインターフェースがバンドルされたもの）がインストールされているのでそのまま使用可能である．現時点での最新バージョンのバイナリは次の URL からダウンロード可能である．
★http://coq.inria.fr/download
その他の重要事項Others
必須ではないが，科目「集合と命題論理」を履修していることが望ましい．また，「セキュアコーディング」「プログラミング言語理論・設計」等の科目と関連が深い．