到達目標
(1) 型システムに基づいた証明支援システムによるプログラミング言語の動作保証の原理を理解し,説明することができる.(定期試験)
(2) 証明支援システムにより動作が保証されたプログラムを記述することができる.(レポート)
ルーブリック
| 理想的な到達レベルの目安 | 標準的な到達レベルの目安 | 未到達レベルの目安 |
型システムとプログラミング | 型システムによる論理記述とプログラミングの関係について,一般論として説明できる | 特定の例については型システムによる論理記述とプログラミングの関係を説明できる | 型システムによる論理記述とプログラミングの関係が説明できない |
証明支援システムによるプログラミング | 証明支援システムを使って高度なプログラミングができる | 証明支援システムを使って簡単なプログラミングができる | 証明支援システムを使ったプログラミングができない |
学科の到達目標項目との関係
学習・教育目標 (E1)
説明
閉じる
JABEE 1(2)(d)(1)
説明
閉じる
教育方法等
概要:
形式手法はコンピュータ・システムの開発に用いられる手法で,数理論理学に基づいた記述言語を使って求められる動作を表現することにより,設計の上流工程の効率化や網羅的な検証を可能にするものである.本講義では,具体的なツールとして証明支援システムCoqを用い,型システムによりある種の動作が保証されたプログラミングを実践する.
授業の進め方・方法:
インターネット上で公開されている書籍 “Software Foundations” (by Benjamin Pierce et al.) とその邦訳(“ソフトウェアの基礎”として公開されている)を中心として進め,区切り毎に内容のまとめや確認問題を行う.
(事前学習)
授業後に公前される講義資料を用いて前回までの内容を復習しておくこと.
注意点:
(履修上の注意)
Coqを用いる箇所については実際に自分のパソコンで動かしてみることが望ましい.
(自学上の注意)
講義資料及び確認問題をwebサイト等で公開するので復習に活用されたい.
評価
(総合評価)
総合評価= 定期試験の平均点 x 0.8 + レポート x 0.2
(単位修得の条件)
総合評価60点以上かつ課せられた全レポート課題のうち60%以上を提出していること.
(再試験について)
60 点に満たない者に対して一度だけ再試験を実施する.
授業の属性・履修上の区分
授業計画
|
|
週 |
授業内容 |
週ごとの到達目標 |
前期 |
1stQ |
1週 |
概要とCoqの紹介 |
授業の導入として,以下の項目に沿って学ぶ: 科目の既要 / Coqについて / 列挙型の記述
|
2週 |
関数プログラミングとプログラムの証明 (1/2) |
以下の項目に沿って学ぶ: introsタクティック / 書き換え(Rewriting)による証明 / Case分析 / Caseへのネーミング
|
3週 |
関数プログラミングとプログラムの証明 (2/2) |
以下の項目に沿って学ぶ: 帰納法 / 形式的証明と非形式的証明 / 証明の中で行う証明
|
4週 |
直積、リスト、オプション (1/3) |
以下の項目に沿って学ぶ: 数のペア / 数のリスト
|
5週 |
直積、リスト、オプション (2/3) |
以下の項目に沿って学ぶ: リストを使ったバッグ / リストに関する推論 / お小言 / リスト上の帰納法 / SearchAbout
|
6週 |
直積、リスト、オプション (3/3) |
以下の項目に沿って学ぶ: オプション / applyタクティック / 帰納法の仮定を変更する
|
7週 |
多相性と高階関数 (1/3) |
ポリモルフィズム(多相性)について理解する
|
8週 |
多相性と高階関数 (2/3) |
データとしての関数について理解する
|
2ndQ |
9週 |
多相性と高階関数 (3/3) |
さらに高度なCoqタクティックについて学ぶ
|
10週 |
命題と根拠 (1/3) |
命題によるプログラミングとその根拠について理解する
|
11週 |
命題と根拠 (2/3) |
帰納法の仮定や帰納的定義について,より深く理解する
|
12週 |
命題と根拠 (3/3) |
CoqのTypeとPropについて理解する
|
13週 |
Coqにおける論理 (1/2) |
Coqにおける全称記号や,真と偽,否定の概念について理解する
|
14週 |
Coqにおける論理 (2/2) |
Coqにおける存在量化子や,同値性の扱い方について理解する
|
15週 |
前期末試験 |
|
16週 |
前期末試験の解答と解説 |
|
モデルコアカリキュラムの学習内容と到達目標
分類 | 分野 | 学習内容 | 学習内容の到達目標 | 到達レベル | 授業週 |
評価割合
| 試験 | レポート | 合計 |
総合評価割合 | 80 | 20 | 100 |
専門的能力 | 80 | 20 | 100 |