ソフトウェア構成特論

ソフトウェアの基礎的な事項、特に、プログラムの形式的扱いにおいて有用な概念である集合の帰納的定義および帰納法、近年有用性が認識されつつあるプログラミング言語の型システム、およびプログラムの意味論について解説を行う。帰納法については整礎帰納法について解説し、数学的帰納法や構造帰納法などはその例であることを示す。型システムについては、関数型言語およびオブジェクト指向言語の核となる部分を対象として具体的な型システムを提示して解説する。意味論は命令型言語、関数型言語、およびオブジェクト指向言語の核となる部分を対象とし、主に操作的意味論について解説する。

授業の目的

この授業を履修することによりソフトウェアの基礎理論（の一部）を身につけることができる。ソフトウェアの検証やテストによりソフトウェアの正しさを（部分的に）示すことが今後ますます重要になってくると考えられ、ソフトウェアの基礎理論はそういったことの根底にある。また、将来新しい言語を開発するような場合に、どのように考えて言語を設計したらいいか、何らかの示唆を与えると考える。

達成目標

1．	集合を帰納的に定義し、帰納法によりその集合に関する簡単な性質を証明できるようになる。
2．	単純な型システムについて、短いプログラムが型について整合性を持つことを示せるようになる。
3．	単純な言語の操作的意味が与えられたとき、短いプログラムの意味を示せるようになる。

授業で使用する言語

授業計画

	【授業計画】	【授業時間外課題（予習および復習を含む）】
1．	集合の帰納的定義	参考書[1]
2．	帰納法 - 整礎帰納法	参考書[1]
3．	帰納法 - 構造帰納法	参考書[1]
4．	帰納法 - 導出に関する帰納法	参考書[1]
5．	操作的意味論 - 単純な命令型言語について	参考書[1]
6．	命令型言語の核言語に関する性質の証明の例	参考書[1]
7．	操作的意味論 - 単純型付きラムダ計算の型システム	参考書[2]
8．	中間試験 - 第1回から第7回までの内容を確認する筆記試験を実施し、終了後解説を行う。（中間試験後、授業の続きを行う。）	第1回から第7回までの内容を復習しておく
9．	型システム - 単純型付きラムダ計算の型システム	参考書[2]
10．	操作的意味論 - 種々の構文を持つ関数型言語の操作的意味論	参考書[2]
11．	型システム - 種々の構文を持つ関数型言語の型システム	参考書[2]
12．	操作的意味論 - Featherweight Javaの操作的意味論	参考書[2]
13．	型システム - Featherweight Javaの型システム	参考書[2]
14．	Featherweight Javaに関する性質について	参考書[2]
15．	・期末試験第1回から第14回までの内容の理解を確認する筆記試験を実施し、終了後解説を行う。	第1回から第14回までの内容を復習しておく。

評価方法と基準

教科書・参考書

以下の本を参考書とする。
[1] Glynn Winskel, The Formal Semantics of Programming Languages --- An Introduction, The MIT Press, 1993.
[2] Benjamin C. Pierce, Types and Programming Langauges, The MIT Press, 2002.
[3] John C. Mitchell, Foundations for Programming Languages, The MIT Press, 1996.
[4] John C. Mitchell, Concepts in Programming Languages, Cambridge University Press, 2002.
[5] Ravi Sethi, Programming Languages --- Concepts & Constructs 2nd edition, Addison Wesley, 1996.

開講部	大学院理工学研究科　修士課程
開講学科	電気電子情報工学専攻
開講学年	1年次
開講時期	前期
単位数	2
単位区分	特修
系列区分	特論
講義区分	講義

1M988200

授業の概要

授業の目的

達成目標

授業で使用する言語

授業計画

評価方法と基準

教科書・参考書

履修登録前の準備

オフィスアワー、質問・相談の方法

環境との関連

地域志向

社会的・職業的自立力の育成

アクティブ・ラーニング科目