南山大学

 
指定
期間
秋学期
単位
年次
3
担当者
張 漢明
他の科目との関連
他学科履修
副題
授業概要 「正しい」プログラムを開発できる能力の養成を目的として、プログラムの正しさの定義から始 め、プログラム の正しさを証明すること、および数学の概念に基づいた形式仕様記述言語を用いて、システムの仕様を記述する方法について学ぶ。プログラムの証明を通じて仕 様の重要性を理解し、仕様を厳密に記述、分析する能力を養う。
学修目標 1. プログラミング言語の持つ種々の基本機能を使ってプログラムを組み立てる方法を知っている 。
2. アルゴリズムの意味を理解しており、簡単なアルゴリズム(探索、整列)のプログラムを知っている。
3. プログラムの正しさとは何かを理解している。
4. 事前条件と事後条件による仕様の記述方法を理解している。
5. Floydの証明法、およびFloyd-Hoare 論理の概念を理解して、単純なプログラムの正しさを証明することができる。
6. 形式仕様記述言語VDM-SLを用いて、単純なシステムの仕様を記述することができる。
授業計画 第1週 プログラムの正しさ
    教科書の1.1,および1.2節を読んでおくこと。
第2週 Floyd の証明法 (部分的正当性)
    教科書の1.3節を読んでおくこと。
第3週 Floyd の証明法(演習)
    Floyd の証明方法を復習しておくこと。
第4週 Floyd の証明法 (停止性)
    教科書の1.4節を読んでおくこと。
第5週 論理の基本
    「情報数学」の論理を復習しておくこと。
第6週 Floyd-Hoare論理 (部分的正当性)
    教科書の2.1節を読んでおくこと。
第7週 Floyd-Hoare論理(演習)
    Floyd-Hoare論理の証明法を復習しておくこと。
第8週 Floyd-Hoare論理 (配列要素)
    教科書の2.2節を読んでおくこと。
第9週 仕様としての事前条件と事後条件
    教科書の3章を読んでおくこと。
第10週 VDM-SL による仕様記述の基本
    教科書の4章を読んでおくこと。
第11週 簡単な仕様記述
    教科書の5章を読んでおくこと。
第12週 実用的な仕様記述
    教科書の6章を読んでおくこと。
第13週 形式仕様記述(演習)
    VDM-SLの記述方法を復習しておくこと。
第14週 形式手法概説
第15週 定期試験
授業時間外の学習(準備学習など) 授業計画欄参照
評価方法 レポート20%、定期試験80%により評価する。
テキスト 教科書 荒木啓二郎、張漢明著 IT Text プログラム仕様記述論 オーム社
参考書 林晋著 プログラム検証論 共立出版
その他 この科目は、次のJABEE 対応コース「情報技術専修コース(情報通信学科・情報システム数理学科)」の学習・教育目標に対応する。(E-3,E-4)