理工学部Faculty of Science and Engineering
COT200XE（計算基盤 / Computing technologies 200）計算の原理Principle of computation
西田 誠幸Seikoh NISHITA
授業コードなどClass code etc
| 学部・研究科Faculty/Graduate school | 理工学部Faculty of Science and Engineering |
| 添付ファイル名Attached documents | |
| 年度Year | 2024 |
| 授業コードClass code | H6162 |
| 旧授業コードPrevious Class code | |
| 旧科目名Previous Class title | |
| 開講時期Term | 春学期集中/Intensive(Spring) |
| 曜日・時限Day/Period | 集中・その他/intensive・other courses |
| 科目種別Class Type | |
| キャンパスCampus | 小金井 |
| 教室名称Classroom name | 担当教員に確認してください |
| 配当年次Grade | 2年 |
| 単位数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)
Course outline: this course focuses on formal methods and mathematical methods, which have become increasingly important as a method of designing secure software without bugs and security holes.
Learning Objectives: the goal of this course are (1) to understand that mathematical logic is an essential tool in the design of secure software, and (2) to be able to perform simple proofs of program correctness using proof support tools.
Learning activities outside of classroom: The standard amount of study outside of class time for preparation and review for each lecture is 4 hours. Students are expected to read through the textbook and video materials in advance and to work on homework assignments. This course will be offered as an intensive course. The textbook and video materials will be available one month prior to the start of the lecture.
Grading Criteria / Policy: Your overall grade in the class will be decided based on the following; Homework in each class: 50%, term-end report : 50%.
授業で使用する言語Default language used in class
日本語 / Japanese
授業の概要と目的（何を学ぶか）Outline and objectives
バグやセキュリティホールのない安全なソフトウェアを設計する手法として近年重要度を増しているフォーマルメソッド（形式手法・数理的技法）について学び、その基本的な考え方を修得します。
到達目標Goal
次の到達目標を掲げます。
1． 安全なソフトウェアの設計に数理論理学が必須のツールであることを理解する
2. 証明支援ツールを用いて、プログラムの正しさに関する簡単な証明を遂行できる
この授業を履修することで学部等のディプロマポリシーに示されたどの能力を習得することができるか（該当授業科目と学位授与方針に明示された学習成果との関連）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. ）
座学の講義とPCを使用した演習を組み合わせた授業形態をとります。演習では証明支援ツールを使って形式的な証明の仕組みと方法について、学生が手を動かしながら学んでもらいます。毎回の講義の中でプログラムの正しさを証明する宿題を出題します。学修の到達度を測るためレポート課題を出題します。オンラインでの開講となった場合の、オンライン授業の方法や各回の授業計画の変更、成績評価方法の変更などについては、学習支援システムでその都度提示します。また、課題等の提出・フィードバックは「学習支援システム」を通じて行います。
アクティブラーニング（グループディスカッション、ディベート等）の実施Active learning in class (Group discussion, Debate.etc.)
なし / No
フィールドワーク（学外での実習等）の実施Fieldwork in class
なし / No
授業計画Schedule
授業形態/methods of teaching：対面/face to face
※各回の授業形態は予定です。教員の指示に従ってください。
1[対面/face to face]：代数的データ型
証明の対象とするデータ型として、真理値型や自然数の代数データ型を導入する。
2[対面/face to face]：簡約による等価性の証明
式の簡約および簡約を利用した等価性の形式的証明について述べる。
3[対面/face to face]：Coq と形式的証明
第1回と第2回で説明した型や演算、証明が証明支援系 Coq で実行できることを確認する。
4[対面/face to face]：帰納法による証明
代数的データ型に関する帰納法とこれを用いた形式的証明について述べる。
5[対面/face to face]：リスト型・直積型・オプション型
リストやペア、オプションなどの構造型を導入する。
6[対面/face to face]：多相性と高階関数
型変数を持つ多相型と、関数を引数や戻り値とする高階関数を導入する。
7[対面/face to face]：Coq におけるタクティック
Coq による形式的証明における指示（タクティック）について説明する。
8[対面/face to face]：論理と形式的証明
Coq の論理的基盤と集合論に基づく論理との違いについて述べる。
9[対面/face to face]：帰納的に定義される命題
帰納的な命題の定義について述べる。また、正規表現に関する定理の証明を説明する。
10[オンライン/online]：マップ型
手続き型言語におけるメモリのモデルとしてマップ型を導入する。
11[オンライン/online]：命令型プログラムにおける証明
抽象構文木の性質を主張する定理の形式的な証明について説明する。
12[オンライン/online]：ホーア論理
プログラムにおける性質の表明とホーアの3つ組、これらを用いたプログラムの性質に関する証明について述べる。
13[オンライン/online]：セキュアコーディング演習
Coq を用いた少し大きな演習に取り組む。
14[オンライン/online]：講義と演習の振り返り
半期の授業内容を振り返り、重要点をまとめる。
授業時間外の学習（準備学習・復習・宿題等）Work to be done outside of class (preparation, etc.)
この科目における1回の講義の準備・復習等の授業時間外学習は、4時間を標準とします。学生は事前にテキストと動画資料に目を通しておくこと、復習として課された宿題に取り組むことの2つが求められます。なお、本科目は集中講義の実施する予定です。テキストと動画資料は講義が開講される1ヶ月前から学生に公開しますので、計画的に資料に目を通しておき、講義1回あたり授業時間外学習4時間を確保してください。
テキスト（教科書）Textbooks
以下のオンライン文書をもとにした講義資料を配布します。
★B.C.Pieace, et al.: Logical Foundations（邦題：論理の基礎）, version 5.6, https://softwarefoundations.cis.upenn.edu/lf-current/index.html, 2019.
参考書References
★萩谷昌己・西崎真也: 論理と計算のしくみ. 岩波書店 (2007). ISBN 978-4-00-006191-9
★鹿島亮: 数理論理学. 朝倉書店 (2009). (証明までふくめて論理学をきちんと学びたい人にぜひおすすめします)
★池渕未来: プログラミングCoq ～絶対にバグのないプログラムの書き方～. http://www.iij-ii.co.jp/lab/techdoc/coqt/
成績評価の方法と基準Grading criteria
先に掲げた到達目標1は各講義回の宿題によって確認します。また、到達目標2については、レポート課題によって確認します。なお、宿題およびレポートを各50%の割合で評価します。
学生の意見等からの気づきChanges following student comments
過去に実施した遠隔授業では提供した動画資料は学生には好評でした。このため、予習として動画資料の視聴できるよう準備します。
学生が準備すべき機器他Equipment student needs to prepare
本講義では Coq（バージョン 8.9.1）を使用します。Coq は貸与PC にすでにインストールされているはずです。受講前に一度確認しておいてください。また、貸与PC以外のPCを使用する場合には、Coq 8.9.1をインストールしてください。なお、インストール方法の説明動画を学習支援システムにて公開します。
その他の重要事項Others
必須ではありませんが、科目「集合と命題論理」を履修していることが望ましいです。また、「離散数学」「データ構造とアルゴリズム」「ソフトウエア工学」「人工知能概論」「形式言語とオートマトン」「論理回路」「数論」等の科目と関連が深いです。