*応用ソフトウェア工学論(修士) [#g8a2231b]
2014年度2Q (A-WS室)
**内容 [#r8273b8f]
-ソフトウェア・テスト with JUnit
-モデル検査 with NuSMV
-関数プログラミング with Haskell
**教科書・参考書 [#pdbae1bd]
***ソフトウェア・テスト (参考書) [#f636dd8b]
-『ソフトウェア・テストの技法』第2版, G.J.Myers 著, 長尾 監訳, 松尾 訳, 近代科学社, ISBN978-4-7649-0329-6, 2006.
-『ソフトウェアのテスト技法』玉井, 松田, 三嶋 共著, 計算機/ソフトウェア技術講座13, 共立出版, ISBN978-4-320-02388-8, 1988.
-『JUnit実践入門 − 体系的に学ぶユニットテストの技法』渡辺 著, 技術評論社, ISBN978-4-7741-5377-3, 2012.
***モデル検査 (教科書) [#p5844a52]
-『モデル検査 初級編』産業技術総合研究所システム検証研究センター 著, ナノオプト・メディア, ISBN978-4-7649-5505-9, 2009.
***関数プログラミング (参考書) [#v149c9a2]
-『関数プログラミング入門 − Haskellで学ぶ原理と技法』R.Bird 著, 山下 訳, オーム社, 978-4-274-06896-6, 2012.
**ソフトウェア・テスト [#v4f3014d]
-スライド
--JUnit, EclEmma - [[junit-ase.pdf:http://www.info.kochi-tech.ac.jp/y-takata/kut-local/junit/junit-ase.pdf]]
--JUnitその2 - [[junit-ase-2.pdf:http://www.info.kochi-tech.ac.jp/y-takata/kut-local/junit/junit-ase-2.pdf]]
--JUnitその3 - [[20140613-Test.pdf:http://www.info.kochi-tech.ac.jp/y-takata/kut-local/junit/20140613-Test.pdf]]
---Myersの三角形 解答編 - [[MyersTriangle8up.pdf:http://www.info.kochi-tech.ac.jp/y-takata/kut-local/junit/MyersTriangle8up.pdf]]
--JUnitその4 - [[20140627-Test.pdf:http://www.info.kochi-tech.ac.jp/y-takata/kut-local/junit/20140627-Test.pdf]]
--参考書 - [[junit-ase-bib.pdf:http://www.info.kochi-tech.ac.jp/y-takata/kut-local/junit/junit-ase-bib.pdf]]
***ソフトウェアテスト 最終課題 [#if27f88f]
--〆切：2014年6月26日(木) 2時限授業開始時
--課題：
---/home/info/y-takata/Public/junit/bowling.zip をインポートし，BowlingScorer#sumUpのテストコードをBowlingScorerTest中に記述しなさい。
---BowlingScorerTest.java中のコメントに書かれた条件や評価の観点を読んで，それらに適合したテストコードを記述すること。
--提出方法：
---テストコードのソースとカバレッジレポートの画像を印刷して提出。
---テストコード中にコメントを書くこと自体は課題の条件ではないが，テスト内容が妥当であることを評価者が理解できるようにしておく必要はある。
--参考資料：
---[[SCAN0004.PDF:http://www.info.kochi-tech.ac.jp/y-takata/kut-local/junit/SCAN0004.PDF]]
***演習の準備 [#d7d32ca7]
-統合開発環境Eclipseの環境設定
--Eclipse → 環境設定
--General → Network Connections → Active ProviderをManualにする
--General → Workspace → Text file encodingをUTF-8にする
-EclipseにJava開発ツール (JDT) をインストール
--Help → Install New Software を選択
--Work with:欄に http://download.eclipse.org/releases/indigo と入力
-- (少し時間がかかるかも)
--一覧の中から Programming Languages → Eclipse Java Development Tools を選択してNextを押す
--ライセンスに同意する
-EclipseにEclEmmaプラグインをインストール
--Help → Eclipse Marketplace を選択
--Find:欄に eclemma と入力してEnterキーを押す
--EclEmma Java Code Coverage が一覧に表示されたら，Installボタンを押す
--ライセンスに同意する
***最初の演習 [#y3278d40]
-Eclipseを使う
--workbench画面にする
--Javaプロジェクトを新規作成（名前は例えば hello）
---File → New → Java Project
--フォルダsrcにJavaクラスを新規作成（例えば Hello）
---フォルダsrcを選択して右クリック (Ctrl + クリック)
---New → Class
--"hello, world" と印字するプログラムを書く
--実行する
---クラスまたはJavaファイルを選択して右クリック (Ctrl + クリック)
---Run As → Java Application
-JUnitを使う準備
--新規プロジェクトを作成（名前は例えば junit）
--フォルダsrcの中にパッケージjunit.tutorialを新規作成
---srcを選択して右クリック
---New → Package
---Name欄に junit.tutorial と入力してFinishを押す
--テスト対象サンプルファイルをjunit.tutorialにコピー
--- Finderのメニューから「移動 → フォルダへ移動」を選ぶ
--- /home/info/y-takata/Public/junit と入力
--- Calculator.java をjunit.tutorialにドラッグ&ドロップ
***Bean Validationを使ったクラスのテスト [#r8ee89fc]
-プロジェクトを外部からインポートする
--File → Import
--General → Existing Projects into Workspace を選んでNextを押す
--Select archive file:欄に /home/info/y-takata/Public/junit/validation.jar と入力してEnterキーを押す
--Projects:欄にてプロジェクトvalidationが選択されていることを確認して，Finishを押す
**モデル検査入門 [#m53b2fbb]
***ダウンロード [#z7258307]
- スライド
-- [[modelcheck.pdf:http://www.info.kochi-tech.ac.jp/y-takata/kut-local/modelcheck/modelcheck.pdf]]
//- 遷移系記述
//-- [[Minilife.smv:http://www.info.kochi-tech.ac.jp/y-takata/kut-local/modelcheck/Minilife.smv]] (4章)
//-- [[VendingMachine.smv:http://www.info.kochi-tech.ac.jp/y-takata/kut-local/modelcheck/VendingMachine.smv]] (11章)
- システム仕様書 (総合課題)
-- 下記の仕様書に従ってモデルを作成し，検証を行いなさい。
--- [[Elevator.txt:http://www.info.kochi-tech.ac.jp/y-takata/kut-local/modelcheck/Elevator.txt]]
***モデル検査 最終課題 [#oe7fcdd9]
--〆切：2014年7月17日(木) 2時限授業開始時
--課題：
---上記の仕様書 Elevator.txt に従ってモデルを作成し，検証を行いなさい。
--提出方法：
---2階建版，3階建版それぞれについて，NuSMVに入力する動作仕様記述とLTL仕様記述を印刷したもの，及び，検証結果 (true or false) とその解釈，反例がある場合は反例を読みやすく整形したもの，を提出する。
---3階建版の動作仕様記述とLTL仕様記述は，2階建版との差分だけでもよい。
---動作仕様記述中にコメントを書くこと自体は課題の条件ではないが，内容が妥当であることを評価者が理解できるようにしておく必要はある。
---Elevator.txt通りに記述した動作仕様では検査項目を満たさない場合は，まずそのことを検証結果の解釈として述べること。その上で，余力があれば，どのように仕様を修正すべきかを述べること。
---Elevator.txtに書かれている情報だけでは動作仕様が決まらない場合は，各自で情報を補うこと。
*** 参考 [#o0a1cf96]
- [[NuSMV home page>http://nusmv.fbk.eu/]]
- [[Spin - Formal Verification>http://spinroot.com/]]
- [[WikiPedia.ja:ライフゲーム]]
- [[WikiPedia.ja:二分決定図]]
**おまけ：SATソルバで遊ぼう [#qcd837e6]
***内容 [#r67a4279]
- 解説 & 演習問題：[[sat-tutorial.html:http://www.info.kochi-tech.ac.jp/y-takata/kut-local/modelcheck/sat-tutorial.html]]
- 演習解答〆切：2014年8月8日(金) 17時 %%6日(水) 22時%%
