[前へ戻る]
   

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

関連するディプロマポリシー Related Diploma Policy
時代の課題と社会の要請に応えた専門的知識と技能/Expert knowledge and skills to address the issues of the age and the demands of society
 
到達目標 Target to be Reached
表示的意味論の基本を理解すること。
To obtain basic understanding of denotational semantics.
 
授業内容 Course Content
使用書(教科書)の第1章から第4章の内容を講義する。
Chapters 1 - 4 of the textbook will be lectured.

本講義は受講者の必要に応じて英語あるいは日本語で開講する。隔年で英和の優先順位を交代させる。本年度は日本語を優先とする。
This unit will be given either in English or Japanese, according to the needs of students. The priority altenates every year: this year, Japanese is given priority.
 
授業計画 Course Planning
1. 述語論理 I / Predicate Logic I
1) 抽象構文 / Abstract Syntax
2. 述語論理 II / Predicate Logic II
1) 述語論理の表示的意味 / Denotational Semantics of Predicate Logic
3. 述語論理 III / Predicate Logic III
1) 正しさと推論 / Validity and Inference
4. 述語論理 IV / Predicat Logic IV
1) 束縛と代入 / Binding and Substitution
5. 単純命令型言語 I / The Simple Imperative Language I
1) 構文 / Syntax
2) 表示的意味 / Denotational Semantics
6. 単純命令型言語 II / The Simple Imperative Language II
1) 領域と連続関数 / Domains and Continuous Functions
7. 単純命令型言語 III / The Simple Imperative Language III
1) 最小不動点定理 / The Least Fixed-Point Theorem
8. 単純命令型言語 IV / The Simple Imperative Language IV
1) 変数宣言と代入 / Variable Declarations and Substitution
9. 単純命令型言語 V / The Simple Imperative Language V
1) 糖衣構文 (syntax sugar): for文 / Syntactic Sugar: The for Command
2) 算術エラー / Arithmetic Errors
3) 健全性と full abstraction / Soundness and Full Abstraction
10. プログラムの仕様とその証明 I / Program Specifications and Their
Proofs I
1) 仕様の構文と意味 / Syntax and Semantics of Specifications
2) 推論規則 / Inference Rules
11. プログラムの仕様とその証明 II / Program Specifications and Their
Proofs II
1) 代入文と逐次合成の規則 / Rules for Asisgnment and Sequential Composition
12. プログラムの仕様とその証明 III / Program Specifications and Their
Proofs III
1) whileコマンドの規則 / Rules fo while commands
13. プログラムの仕様とその証明 IV / Program Specifications and Their
Proofs IV
1) その他の規則 / Further Rules
2) フィボナッチ数の計算 / Computing Fibunacci Numbers
3) 高速冪乗計算 / Fast Exponentiation
4) 微妙な問題と、この手法の限界 / Complications and Limitations
14. 配列 / Arrays
1) 抽象構文 / Abstract Syntax
2) 表示的意味 / Denotational Semantics
3) 二分探索法 / Binary Search
4) 配列のための推論規則 / Inference Rules for Arrays
5) 配列についての高階述語 / Higher-Order Assertions About Arrays
 
授業運営 Course Management
講師による講義の他、受講生による発表を適宜課して、能動的な参加を促す。演習問題を課題として適宜与える。
In addition to the talks by the lecturer, exercises are given to the students who are asked to give presentations on them, thus encouraging active participance to the course.
 
評価方法 Evaluation Method
平常の課題解答の結果に基づいて評価する.
Marks are given according to the evaluation of the submitted solutions to the exercises.
 
オフィスアワー Office Hour (s)
火曜日13:30-15:00 2-226 (木下)
なお、これ以外の時刻でもメイルなどで面談の約束を受け付けるので、積極的な質問や相談を歓迎する。
Tuesday 13:30-15:00 2-226
Appointments in other periods may be accepted via e-mail.
 
使用書 Textbook (s)
John Reynolds『Theories of Programming Languages』[Cambridge University Press]1998


 
 
 
[前へ戻る]