到達目標
・ソフトウェア検証の一手法である形式手法の基本的概念を理解できる。
・Alloyの基礎的な文法及び解析法を理解し，それを用いて基礎的な事例を解析できる。
ルーブリック
| 理想的な到達レベルの目安 | 標準的な到達レベルの目安 | 最低限レベルの目安(可) | 未到達レベルの目安 |
| ソフトウェ検証の一手法である形式手法の概念に関する理解 | 形式手法の概念が理解でき，それを応用した解析が可能である。 | 形式手法の概念が理解でき，それを用いた基礎的な解析が可能である。 | 形式手法の概念が理解できる。 | 形式手法の概念が理解できない。 |
| Alloyに関する理解 | Alloyの基礎的な文法及び解析法を理解し，それを応用した事例解析ができる。 | Alloyの基礎的な文法及び解析法を理解し，それを用いて基礎的な事例を解析できる。 | Alloyの基礎的な文法及び解析法を理解できる。 | Alloyの基礎的な文法及び解析法を理解できない。 |
学科の到達目標項目との関係
教育方法等
概要:
ソフトウェアを正しく構築するために必須であるソフトウェア検証に関し，ソフトウェア検証で用いられる手法の一つである形式手法をAlloyを用いて修得する。ソフトウェアの正しさに関する様々な概念を学び，正しさの解析をAlloyを用いて演習する。
授業の進め方・方法:
教科書及びパワーポイントスライドを用いて関連知識の習得し，修得した知識を基にAlloyツールを用いて演習する。
注意点:
・演習にはAlloyツールを用いるため，Alloyツールの実行環境が必要である。
・演習にあたっては，授業時間の他にも，昼休みや放課後を利用して自主的に行うことが望まれる。
・理論的背景として情報数学の知識が使われるため，情報数学に関する科目を受講していることが望ましい。
授業計画
|
|
週 |
授業内容 |
週ごとの到達目標 |
| 前期 |
| 1stQ |
| 1週 |
ガイダンス，環境構築 |
Alloyの実行環境を構築し，簡単な例題を実行できる。
|
| 2週 |
Alloy文法 |
Alloyの簡単な文法を理解し，簡単な例題を記述できる。
|
| 3週 |
Alloy解析 |
Alloyの関連な例題を解析できる。
|
| 4週 |
Compositeパターン |
Compositeパターンを理解し，それを用いた簡単な例題を記述できる。
|
| 5週 |
抽象データの表現と解析 |
抽象データの表現を理解し，それを用いた簡単な例題を解析できる。
|
| 6週 |
機能仕様の表現と解析 |
機能仕様の表現を理解し，それを用いた簡単な例題を解析できる。
|
| 7週 |
Alloy入門のまとめ |
抽象データの表現と機能仕様の表現を用いて，例題を表現・解析できる。
|
| 8週 |
Alloyを用いた解析１ |
Alloyを用いて，具体的な事例を記述し，解析できる。
|
| 2ndQ |
| 9週 |
Alloyを用いた解析２ |
Alloyを用いて，具体的な事例を記述し，解析できる。
|
| 10週 |
Alloyの基礎 |
Alloyの基礎理論を理解し，解析に活用できる。(37ページのスコープを増やす例)
|
| 11週 |
手続きとデータ構造 |
手続きとデータ構造を理解し，Alloyを用いて記述できる。
|
| 12週 |
正しさの基準 |
正しさの基準を理解し，Alloyを用いて記述できる。
|
| 13週 |
リファインメントの基礎 |
リファインメント関係を理解し，Alloyを用いて記述できる。
|
| 14週 |
リファインメント検査 |
リファインメント検査を理解し，Alloyを用いて解析できる。
|
| 15週 |
期末試験 |
期末試験の解説を行う。
|
| 16週 |
|
|
モデルコアカリキュラムの学習内容と到達目標
| 分類 | 分野 | 学習内容 | 学習内容の到達目標 | 到達レベル | 授業週 |
| 専門的能力 | 分野別の専門工学 | 情報系分野 | プログラミング | 与えられたソースプログラムを解析し、プログラムの動作を予測することができる。 | 4 | |
| ソフトウェア | ソースプログラムを解析することにより、計算量等のさまざまな観点から評価できる。 | 4 | |
| 同じ問題を解決する複数のプログラムを計算量等の観点から比較できる。 | 4 | |
| 情報数学・情報理論 | 離散数学に関する知識をアルゴリズムの設計、解析に利用することができる。 | 4 | |
評価割合
| 試験 | 発表 | 相互評価 | 態度 | ポートフォリオ | レポート | 合計 |
| 総合評価割合 | 50 | 0 | 0 | 0 | 0 | 50 | 100 |
| 基礎的能力 | 20 | 0 | 0 | 0 | 0 | 20 | 40 |
| 専門的能力 | 30 | 0 | 0 | 0 | 0 | 30 | 60 |
| 分野横断的能力 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |