南山大学

文字サイズ
 
指定
 選
期間
 春学期
単位
 ２
年次
 1
担当者
 張　漢明
講義題目
開講キャンパス 瀬戸キャンパス　サテライトキャンパス
講義内容 計算機プログラムの数理モデルに対する形式手法をもとに，プログラムの正しさを形式的に示すための基礎理論と解析手法について学ぶ。講義では，仕様記述および実現プログラムそれぞれの妥当性の確認や相互整合性の検証などの例を通じて，ソフトウェアの信頼性向上のための基盤について学ぶ。
学修目標 １．プログラムの正しさを形式的に示すことについて，その役割と意義を説明できる。
２．計算機プログラムの数理モデルなどの，形式手法において用いられる概念や用語の意味を説明できる。
３．プログラムの正しさを示すための解析手法や，その基となる基礎理論の概略について理解している。
４．仕様記述および実現プログラムにおける妥当性の確認手法について，その概略を知っている。
５．仕様記述および実現プログラム間の相互整合性の検証手法について，その概略を知っている。
講義計画 第 1 〜 2 週計算機プログラムの数理モデルと形式手法
第 3 〜 5 週プログラムの正しさ
第 6 〜 10 週システム仕様記述法
第 11 〜 15 週仕様記述検証法
評価方法 授業中の演習およびレポートによる評価。必要があれば筆記試験を行う。
テキスト
その他