|
プログラム理論特論
|
|
| 担当教員 |
水谷哲也、亀山幸義
|
| 電子メール | 水谷哲也:mizutani, 亀山:kam (それぞれの後に @cs.tsukuba.ac.jpをつけること） |
| URL | |
| オフィスアワー | 授業の始めに連絡する。 |
| 科目番号 | 01CH213 |
| 分野 | 知能ソフトウェア |
| 基礎／専門の別 | |
| 授業形態 | 講義 |
| 開講学期 | 秋A |
| 時限 | 金5,6 |
| 教室 | |
| キーワード | 記号論理、意味論、仕様記述、検証、 ホーア論理、実時間プログラム系 |
| Keyword | Symbolic Logic, Specification, Verification, Semantics, Hoare Logic, Realtime Systems. |
| 前提条件 | 必須ではないが、命題論理，述語論理とプログラム言語の基礎的事項を理解していると講義を理解しやすい。 |
| 学習目標 | プログラムの理論的基礎を学ぶことを目的とし，形式的仕様記述及び検証の概念及び方法を習得する． |
| 概要 | Hoare論理による手続き型プログラムの検証,実時間プログラム系の仕様記述および検証などを通じてプログラムの理論的基礎を深く探究する. |
| 授業計画 | 第１回：一階述語論理の基礎 （水谷） 第２回：Hoare論理によるプログラムの仕様記述 （水谷） 第３回：Hoare論理によるプログラムの検証 （水谷） 第４回：実時間プログラム系の仕様記述 （水谷） 第５回：実時間プログラム系の仕様の検証 （水谷）、プログラム検証への応用（亀山） |
| 教科書 | 授業中に配布する |
| 参考書 | M. Huth and M. Ryan, "Logic in Computer Science (Second Edition)", Cambridge Univ. Press, 2004. |
| 成績評価 | 出席を前提とし，演習，レポート，期末試験の結果を総合して判定する． |
| TF・TA | |
| その他の情報 | |