A この講義ではプログラムの形式的意味論と仕様記述、検証論について学びます。 計算機プログラムの意味を数学的に厳密に取り扱い、プログラムの停止性、同等性などを論じるのがプログラムの形式的意味論です。 また、形式的仕様記述では、プログラムの動作を数学的に与える方法を提供します。 これらの土俵の上に、検証論では、プログラムが誤りなく仕様を満たしていることを証明する手段を与えます。 計算機に関する基本的な概念、「情報数学基礎論A,B」などの計算機数学の基礎、「数理論理学A,B」などの記号論理学の知識を仮定しています。
B 計算の基礎理論についての講義を予定しています．
備考:理系向けです。 数理情報論分野あるいは、数理と情報コースで計算機を専門とする学生は2回生または3回生で履修することが望ましいといえます。
レポートにより成績評価を行なう予定です。