| 科目名 |
応用ソフトウェア工学論 |
| 担当教員 |
高田 喜朗,松崎 公紀 |
| 対象学年 |
1年,2年 |
クラス |
院：専門001 |
| 講義室 |
|
開講学期 |
１学期 |
| 曜日・時限 |
時間外 |
単位区分 |
選択 |
| 授業形態 |
一般講義 |
単位数 |
2 |
| 準備事項 |
|
| 備考 |
|
| 授業の詳細1 |
授業の目的
ソフトウェア工学の第一の目的は，品質のよい，信頼性の高いソフトウェアを効率よく開発することと言える。情報システムが広く社会に浸透し，ソフトウェアの信頼性への要求はますます高まっている。ソフトウェアの信頼性を高める技術として，本科目では形式的検証法と関数プログラミングを取り上げる。現在のソフトウェア開発現場ではこれらの技術は必ずしも普及しているとは言えないが，どちらも大規模化・複雑化する要求に破綻なく立ち向かう鍵の一つとして注目されており，これらの知識を持つ技術者の必要性が今後増していくと考えられる。これらの技術の基礎を理解し，基本的な手法を実践できるようになることが，本科目の目的である。 |
| 授業の詳細2 |
授業の概要
キーワード：形式的検証, モデル検査, Spin, NuSMV, 関数プログラミング, Haskell
本科目は2つの部分で構成される。
前半は高田が担当し，形式的検証法，特にモデル検査法について学習する。
後半は松崎が担当し，関数プログラミングについて学習する。
いずれも講義形式で基本事項を学んだ後，演習によって理解を深める。
達成目標
- 形式的検証，関数プログラミングとはそれぞれ何か，ソフトウェア開発においてどのような意義があるか，説明できる。
- モデル検査の理論的基礎を理解し，検証結果が何を意味しているか（能力と限界）を説明できる。
- モデル検査ツールを使って実際に簡単な検証を行える。
- 高階関数や再帰構造を多用する関数プログラミングの作法を理解し，関数型言語を使って実際にプログラムを作成できる。 |
| 授業の詳細3 |
授業計画
1. オリエンテーション
2―7. 形式的検証
2. さまざまな形式的検証法
3. モデル検査とは
4. 演習：簡単なモデル検査
5. 演習：さまざまな例題
6. 時相論理式
7. 演習：自動販売機
8―15. 関数プログラミング
8. 基本的な概念
9. 基本データ型
10. リスト
11. 演習：リスト処理の例
12. 演習：カレンダーの印刷
13. 再帰法と帰納法
14. 無限リスト
15. 演習：探索と数え上げ |
| 授業の詳細4 |
教科書
下記の2冊をそれぞれ前半・後半で用いる。
- 『モデル検査 初級編』産業技術総合研究所システム検証研究センター著, ナノオプト・メディア, ISBN978-4-7649-5505-9 (2009).
- 『関数プログラミング』Bird, Wadler共著, 武市訳, 近代科学社, ISBN978-4-7649-0181-0 (1991).
成績評価
レポートに基づいて評価する。
AA: レポートの完成度も含めて上記の達成目標を完全に達成したと認められる場合
A: 上記の達成目標に十分到達したと認められる場合
B: 上記の達成目標を概ね達成したと認められる場合
C: モデル検査および関数プログラミングとは何かを説明でき，簡単な検証や関数型言語によるプログラム作成を行えると認められる場合
F: 上記Cに到達しない場合
備考
連絡先：A棟470室 |
| 授業の詳細5 |
|
| 授業の詳細6 |
|
| 授業の詳細7 |
|
| 授業の詳細8 |
|
| 授業の詳細9 |
|
| 授業の詳細10 |
|
|