[前へ戻る]
   

 授業科目
 Course Title
プログラム意味論
Programming Semantics
 担当者
 Instructor
教授   木下 佳樹  前学期 金曜日2時限
講師   武山 誠  前学期 金曜日2時限
 単 位
 Credit
2

到達目標 Target to be Reached
システム妥当性確認に関する基本的な理解を得ること
 
授業内容 Course Content
使用書(教科書)の第1章から第4章の内容を講義する.
1. 述語論理
1) 抽象構文
2) 述語論理の表示的意味
3) 正しさと推論
4) 束縛と代入
2. 単純命令型言語
1) 構文
2) 表示的意味
3) 領域と連続関数
4) 最小不動点定理
5) 変数宣言と代入
6) 糖衣構文 (syntax sugar): for文
7) 算術エラー
8) 健全性と full abstraction
3. プログラムの仕様とその証明
1) 仕様の構文と意味
2) 推論規則
3) 代入文と逐次合成の規則
4) whileコマンドの規則
5) その他の規則
6) フィボナッチ数の計算
7) 高速冪乗計算
8) 微妙な問題と,この手法の限界
4. 配列
1) 抽象構文
2) 表示的意味
3) 二分探索法
4) 配列のための推論規則
5) 配列についての高階述語
 
授業計画 Course Planning
1. 述語論理 I
1) 抽象構文
2. 述語論理 II
1) 述語論理の表示的意味
3. 述語論理 II
1) 正しさと推論
4. 述語論理 II
1) 束縛と代入
5. 単純命令型言語
1) 構文
2) 表示的意味
6. 単純命令型言語
1) 領域と連続関数
7. 単純命令型言語
1) 最小不動点定理
8. 単純命令型言語
1) 変数宣言と代入
9. 単純命令型言語
1) 糖衣構文 (syntax sugar): for文
2) 算術エラー
3) 健全性と full abstraction
10. プログラムの仕様とその証明
1) 仕様の構文と意味
2) 推論規則
11. プログラムの仕様とその証明
1) 代入文と逐次合成の規則
12. プログラムの仕様とその証明
1) whileコマンドの規則
13. プログラムの仕様とその証明
1) その他の規則
2) フィボナッチ数の計算
3) 高速冪乗計算
4) 微妙な問題と,この手法の限界
14. 配列
1) 抽象構文
2) 表示的意味
15. 配列
1) 二分探索法
2) 配列のための推論規則
3) 配列についての高階述語
 
授業運営 Course Management
講師による講義の他、受講生による発表を適宜課して、能動的な参加を促す。
演習問題を課題として適宜与える。
 
評価方法 Evaluation Method
平常の課題解答の結果に基づいて評価する。
 
オフィスアワー Office Hour (s)
金曜日13:30~15:00 2-226 (木下)

 
使用書 Textbook (s)
John Reynolds,Theories of Programming Languages,Cambridge University Press,1998


 
 
 
[前へ戻る]