南山大学　シラバス検索用

他の科目との関連
他学科履修	可
副題
講義内容	「正しい」プログラムを開発できる能力の養成を目的として、プログラムの正しさの定義から始め、既にあるプログラムの正しさを証明すること、およびプログラミング作業を数学的に行うことの理論と手法を講義する。
講義計画	１．プログラムの検証入門プログラムの正しさとそれを保証する方法について説明する。プログラムの正しさを証明するためのFloydの方法と、Floydの方法を数学的な証明体系として再構成した公理系であるHoare理論を紹介する。２．形式仕様記述入門プログラムの使用を、数学の概念を用いて簡潔かつ厳密に記述する方法について説明する。形式仕様言語ZやVDM等を用いて、具体例を通して形式的な仕様の書き方と概念を学ぶ。
評価方法	レポート及び定期試験が評価の対象となる。
テキスト	IT　Text　プログラム仕様記述論　オーム社【その他】他学科の学生が履修する場合は、ネットワークに接続できて、wwwページを見ることのできるノートPCをもっていることを条件とする。
その他