[前へ戻る]
   

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

到達目標 Target to be Reached
算譜意味論、つまりプログラミング言語の数理科学的なモデルの基本的な理解を得ることを目標とする。

 
授業内容 Course Content
CやJavaなどの、いわゆる命令型プログラミング言語の本質的な機能だけを抜き出した「whileプログラム」について、操作的意味論と公理的意味論を紹介し、二つの意味論の関係を論じる。
 
授業計画 Course Planning
1. 算譜意味論とは? 【操作的意味論と公理的意味論】
2. 命題と述語1 【状態、状態における述語の真偽、トートロジー、命題を状態の集まりとみる】
3. 述語の証明 【自然演繹、等式の公理】
4. 述語の証明2 【形式的証明を書く】
5. 述語2 【状態の範囲を拡げる、自由変数と束縛変数、代入、限量】
6. 述語の証明3 【限量記号のついた命題の証明】
7. 自然数と配列 【自然数の定義と公理、配列の定義と公理】
8. while言語とその操作的意味1【述語変換wp、skip命令、abort命令、命令の逐次合成、単純変数への代入命令、単純変数への多重代入命令、配列要素への代入命令、一般的な多重代入命令】
9. while言語とその操作的意味2【分岐命令、繰り返し命令】

10. 述語変換と最弱事前条件による公理的意味1【述語変換】
11. 述語変換と最弱事前条件による公理的意味2【最弱事前条件】
12. 操作的意味から公理的意味へ1【操作的意味論において公理が成り立つことの証明】
13. 公理的意味から操作的意味へ【公理的意味論から操作的意味論を構成する】
14. 集合の帰納的定義
15. 集合の余帰納的定義

 
授業運営 Course Management
講義と演習による。人数によってはセミナー形式とする。随時レポートを提出させる。

 
評価方法 Evaluation Method
提出物および講義、演習での応答似よって評価する。
 
オフィスアワー Office Hour (s)
金曜日13:30-15:00、2-226(変更ある場合には講義などで通知する。)

 


 
 
 
[前へ戻る]