南山大学　シラバス検索用

指定	選	期間	秋学期
単位	２	年次	3
担当者	張　漢明

他の科目との関連
他学科履修	可
副題
授業概要	「正しい」プログラムを開発できる能力の養成を目的として、プログラムの正しさの定義から始め、プログラムの正しさを証明すること、および数学の概念に基づいた形式仕様記述言語を用いて、システムの仕様を記述する方法について学ぶ。プログラムの証明を通じて仕様の重要性を理解し、仕様を厳密に記述、分析する能力を養う。
学修目標	１．プログラミング言語の持つ種々の基本機能を使ってプログラムを組み立てる方法を知っている。２．アルゴリズムの意味を理解しており、簡単なアルゴリズム（探索、整列）のプログラムを作成することができる。３．プログラムの正しさとは何かを理解している。４．事前条件と事後条件による仕様の記述方法を理解している。５．Floydの証明法、およびFloyd-Hoare論理の概念を理解して、例題プログラムの正しさを証明することができる。６．形式仕様記述言語VDM-SLを用いて、例題システムの仕様を記述することができる。
授業計画	第１週　形式手法の概要第２週　プログラムの検証第３週　Floydの証明法（部分的正当性）第４週　Floydの証明法（停止性）第５週　演習I（Floydの証明法）第６週　論理の基本第７週　Floyd-Hoare論理（部分的正当性）第８週　Floyd-Hoare論理（配列要素）第９週　演習II（Floyd-Hoare論理）第10週　仕様としての事前条件と事後条件第11週　VDM-SLによる仕様記述の基本第12週　例題の仕様記述第13週　実用的な仕様記述第14週　演習III（形式仕様記述）第15週　定期試験
評価方法	授業中に行なう演習（３回） 50%、定期試験50%で評価する。
テキスト	教科書　荒木啓二郎、張漢明（著）、IT Textプログラム仕様記述論、オーム社、2002。参考書　林　晋（著）、プログラム検証論、共立出版、1995。
その他	この科目は、次のJABEE対応コース「情報技術専修コース（情報通信学科・情報システム数理学科）」の学習・教育目標に対応する。（E）