|
プログラム理論特論
|
|
| 担当教員 |
水谷哲也、亀山幸義
|
| 電子メール | 水谷哲也:mizutani, 亀山:kam (それぞれの後に @cs.tsukuba.ac.jpをつけること） |
| URL | |
| オフィスアワー | F708 木15:15-16:30.(要アポイントメント) |
| 科目番号 | 01CH213 |
| 分野 | 知能ソフトウェア |
| 基礎／専門の別 | |
| 授業形態 | 講義 |
| 開講学期 | 秋A |
| 時限 | 金5,6 |
| 教室 | 3B302 |
| キーワード | 記号論理、意味論、仕様記述、検証、 ホーア論理、ガード付きコマンド，非決定的プログラム |
| Keyword | Symbolic Logic, Specification, Verification, Semantics, Hoare Logic, Guarded commands, Non-Determinacy. |
| 前提条件 | 必須ではないが、命題論理，述語論理とプログラム言語の基礎的事項を理解していると講義を理解しやすい。 |
| 学位プログラム・コンピテンスとの関係 | 知の活用力,知識力 |
| 学習目標 | プログラムの理論的基礎を学ぶことを目的とし，形式的仕様記述及び検証の概念及び方法を習得する． |
| 概要 | Hoare論理による手続き型プログラムの検証,実時間プログラム系の仕様記述および検証などを通じてプログラムの理論的基礎を深く探究する. |
| 授業計画 |
第1回：基本概念 第2回：whileプログラムの構文と意味論，Hoare論理によるプログラムの部分的正当性の検証 第3回：Hoare論理によるプログラムの完全正当性の検証，健全性 第4回：Hoare論理の完全性，証明アウトライン 第5回：ガード付きコマンドを用いた非決定的プログラムの意味論と検証 |
| 教科書 |
Apt, K. R., de Boer, F. S. and, Olderog, E-R. : "Verification of Sequential and Concurrent Programs, 3rd edition, Springer-Verlag, 2009. 内容は配布pdfでカバーするので購入する必要はない |
| 参考書 |
M. Huth and M. Ryan, "Logic in Computer Science (Second Edition)", Cambridge Univ. Press, 2004. 林晋: "プログラム検証論", 共立出版, 1995. |
| 成績評価 | 出席を前提とし，演習およびレポートの結果を総合して判定する．期末試験は行わない． |
| TF・TA | |
| その他の情報 | 日本語で講義を行う． TA，TFはいない予定． |