授業の目的 【日本語】
Goals of the Course(JPN) | | | ソフトウェア検証の厳密化や自動化のためには，プログラミング言語を形式的に理解することが必須である。この講義では，プログラミング言語とプログラムを数学的対象として形式的に捉え，解析する手 法について理解することを目的とする。 |
|
|
授業の目的 【英語】
Goals of the Course | | | We learn the mathematical foundation of the theory of programming languages for program verification and analysis: operational semantics, denotational semantics, and program logic such as Hoare logic and separation logic. |
|
|
到達目標 【日本語】
Objectives of the Course(JPN) | | | 授業終了時に受講者は以下の知識を身に付けている：プログラミング言語の形式意味論（操作的意味論，表示的意味論），プログラム論理（ホーア論理，分離論理）の基礎． |
|
|
到達目標 【英語】
Objectives of the Course | | |
|
授業の内容や構成
Course Content / Plan | | プログラミング言語およびプログラムの意味を厳密に捉え，解析する手法の基礎について学ぶ．具体的には，簡単なプログラミング言語に対する種々の意味論と，プログラムの性質を記述・検証するための論理について学ぶ．プログラムとその意味を数学的に定義することの意義と，これらの概念がプログラム解析やプログラム検証の基礎となることを解説する．
〔計画〕
1. ガイダンス
2. 様々な帰納法
3. 操作的意味論
4. 公理的意味論（ホーア論理）
5. 分離論理
6. 領域理論と表示的意味論 | |
|
|
履修条件・関連する科目
Course Prerequisites and Related Courses | | | 情報学部科目の論理学1, 2cを受講していることが望ましい． | |
|
|
成績評価の方法と基準
Course Evaluation Method and Criteria | | | 数回のレポート課題の評価50%，期末の筆記試験50%，合計100点満点で60点以上を合格とする．ただし，大学の授業実施方針の状況によっては，期末の筆記試験に代えてレポートによる評価を行なうことがある． | |
|
|
教科書・参考書
Textbook/Reference book | | 参考書：G.ウィンスケル「プログラミング言語の形式的意味論入門」（丸善）
（もしくは，原著 G.Winskel "The Formal Semantics of Programming Languages, An Introduction" (MIT Press）
その他，必要に応じて資料を配布する。 | |
|
|
課外学習等（授業時間外学習の指示）
Study Load(Self-directed Learning Outside Course Hours) | | | 各回の授業内容を復習し，レポート課題を提出すること． | |
|
|
授業開講形態等
Lecture format, etc. | | |
|
遠隔授業（オンデマンド型）で行う場合の追加措置
Additional measures for remote class (on-demand class) | | |
|