7.3 テストケースの自動生成

7.3.1 ソフトウェアのテスト技術

テスト：

• 動的 （←→ ？）

• 事後検査 （←→ ？）

P.185中～

P.186上～

テストで全ケースを網羅することはできない

P.186中～

カバレッジ測定の指標がいくつかある

7.3.2 仕様に基づくテストケース自動生成

(1) コントラクトの利用

SBT: Specification Based Testing

P.187中～

一様性仮定： x>1という事前条件ならx=2でも3でも同様の動きだろう

P.187下～

DNF(Disjuncitive Normal Form)分割

P.188上～

重なりのない領域に分ける

P.188中～

カウンタ

P.188下～

P1とP4は解なし

P.189下～

期待しない入力値を入れてみる

P.190上～

論理式＋境界値分割

P.190中～

[ex14-1] 一般的なソフトウェアのテストがあてはまらないものはどれですか

[ex14-2] SBTの代表的な手法としてDNF分割があるが、なぜ分割する必要がありますか

(2) 構造データの系統的生成

入力データが木構造だったら？

P.192上～

構造データのあるべき姿をていねいに記述する

7.3.3 モデル検査の利用

モデル検査の反例から対応するテストデータが得られる

→ テストで到達させたい状態にもっていける

P.192中～

トラップ性質：□(￢P(v))

P.192下～

assert(false)が使えるならより簡単

P.192下～

カバーできてない箇所にトラップを入れる

P.193上～

トラップ変数を使う方法 → どの経路を通ってきたのか？

P.193下～

到達できるが冗長かもしれない

[ex14-3] 特定の状態についてのテストデータを得る際に最も合理的な方法はどれですか

[ex14-4] モデル検査の反例として得られるテストデータのデメリットはどれですか

教科書（図はすべてこちらより引用）：
　中島震，「形式手法入門―ロジックによるソフトウェア設計―」，オーム社