2024年度 学院等開講科目 情報理工学院 情報工学系 情報工学コース
プログラム理論
- 開講元
- 情報工学コース
- 担当教員
- 西崎 真也
- 授業形態
- 講義 (ハイフレックス型)
- メディア利用科目
- -
- 曜日・時限
(講義室) - 月3-4 (WL1-301(W531)) / 木3-4 (WL1-301(W531))
- クラス
- -
- 科目コード
- CSC.T422
- 単位数
- 200
- 開講時期
- 2024年度
- 開講クォーター
- 1Q
- シラバス更新日
- 2025年3月14日
- 使用言語
- 英語
シラバス
授業の目的（ねらい）、概要
プログラム理論とは，プログラムの振る舞いを理解・説明するための基礎となる理論である．本講義では，操作的意味論， 表示的意味論， 公理的意味論の3つの理論についてそれぞれ学び，プログラムの振舞いや性質を形式的に検証する方法について学ぶ．それぞれの理論の応用として，ドメイン理論について学ぶ．
到達目標
本講義では，プログラミング言語の代表的な意味定義手法である操作的意味論， 表示的意味論， 公理的意味論の3つの理論について学び，それらを情報処理分野において応用するための基礎を築くことを目的とする．
本講義を履修することによって，プログラミング言語の形式的な意味定義法について理解し，
理論に基づいてプログラムの検証を行う際に必要となる証明法を理解し身につける．
また，プログラミング言語の形式的な取り扱いやプログラムの振舞いを検証する方法を情報処理分野において応用できるようになることを目標とする．
キーワード
操作的意味論，表示的意味論，公理的意味論，帰納法の原理, ホーア論理，ドメイン理論，並行計算モデル。
学生が身につける力
- 専門力
- 教養力
- コミュニケーション力
- 展開力 (探究力又は設定力)
- 展開力 (実践力又は解決力)
授業の進め方
座学. 基本概念と各意味論の諸定義を学んだ後に例題を用いて証明方法を学ぶ。
授業計画・課題
| 授業計画 | 課題 | |
|---|---|---|
| 第1回 | プログラムの意味論とは | プログラムの意味論の必要性を理解できる |
| 第2回 | 基本概念 | 基本概念を説明できる |
| 第3回 | 操作的意味論 ( 式の評価，コマンドの実行 ） | 操作的意味論 ( 式の評価，コマンドの実行 ）を説明できる |
| 第4回 | 種々の帰納的定義と帰納法原理 | 種々の帰納的定義と帰納法原理を説明できる |
| 第5回 | 操作的意味論における証明 | 操作的意味論における証明を説明できる |
| 第6回 | 表示的意味論 | 表示的意味論を説明できる |
| 第7回 | 操作的意味論と表示的意味論の関係 | 操作的意味論と表示的意味論の関係を説明できる |
| 第8回 | 公理的意味論，Hoare 論理 | 公理的意味論，Hoare 論理を説明できる |
| 第9回 | Hoare 規則の健全性と完全性 | Hoare 規則の健全性と完全性を説明できる |
| 第10回 | プログラムの検証 | プログラムの検証を説明できる |
| 第11回 | ドメイン理論 (1) 諸定義 | ドメイン理論 諸定義を説明できる |
| 第12回 | ドメイン理論 (2) ドメイン理論の諸性質 | ドメイン理論と諸性質を説明できる |
| 第13回 | 並行計算のモデル：定義 | 並行計算のモデルの諸定義を説明できる |
| 第14回 | 並行計算のモデル：例 | 並行計算のモデルを例を通して理解している |
準備学修(事前学修・復習)等についての指示
学修効果を上げるため，教科書や配布資料等の該当箇所を参照し，「毎授業」授業内容に関する予習と復習（課題含む）をそれぞれ概ね100分を目安に行うこと。
教科書
特になし. 講義スライドを配布．
参考書、講義資料等
Semantics with Applications: An Appetizer, Riis Nielson, Hanne, Nielson, Flemming ， Springer ， 2007
Communicating and mobile systems: the pi-calculus, Robin Milner, Cambrdge University Press.
成績評価の方法及び基準
小レポート(40%)・期末試験(60%)により評価する。ただ、新型コロナの再拡大等の理由により期末試験は期末レポートに変わる場合がある。
関連する科目
- CSC.T261 ： 情報論理
- MCS.T416 ： 論理と計算
履修の条件・注意事項
数理論理学