Disciplined Software Engineering Lecture #12

Disciplined Software
Engineering
Lecture #12
Software Engineering Institute
Carnegie Mellon University
Pittsburgh, PA 15213
Sponsored by the U.S. Department of Defense
Copyright © 1994 Carnegie Mellon University1
設計検証
設計検証は2つの講義でカバーされる。この講義では
以下を述べる。
•設計検証する理由
•状態機械の正しさ
•実行表
•帰納法による証明
次の講義は以下をカバーする
•トレース表
•数学的プログラムの検証
•プログラムの証明
Copyright © 1994 Carnegie Mellon University2
設計検証の必要性- 1
ＰＳＰを改善しつつ作業を行うが、設計の欠陥数を顕著
に減少させることは難しいと自覚するだろう。
チェックリストを使い、注意力を集中化すれば、コードレ
ビューによる欠陥摘出率を改善できる。
設計レビューによる欠陥摘出率を改善するには、設計
検証手法の規範を使う必要がある。
Copyright © 1994 Carnegie Mellon University3
ｺｰﾃﾞｨﾝｸﾞ時に作り込まれた欠陥
- 範囲
250
欠陥数 /KLOC
200
Max
150
Avg.
100
Min
50
0
1
2
3
4
5
6
7
8
9
10
プログラム番号
Copyright © 1994 Carnegie Mellon University4
設計時に作り込まれた欠陥
- 範囲
100
欠陥数 /KLOC
90
80
70
60
Max
50
Avg
40
30
Min
20
10
0
1
2
3
4
5
6
7
8
9
10
プログラム番号
Copyright © 1994 Carnegie Mellon University5
設計検証の必要性- 2
設計検証に対するきちんとしたアプローチが本質的で
ある。なぜならば
•よくある設計欠陥は、条件が見落とされることによっ
て引き起こされる→こうした事例は多い。
•ありそうもない状況のように見えることが重要なシス
テムにおいて起こりやすくなっている
•最初のプログラムバージョンでは起こり得なかった状
況が後の修正によって引き起こされることがある。
Copyright © 1994 Carnegie Mellon University6
設計検証の必要性- 3
構造化された設計検証の手法に従うことによって、以
下の可能性が増す：
•見落とされた条件に気がつく
•まれにしか露出しないリスクを確認する
•将来起こりうる危険を認識する
設計レビューに関するデータを記録することによって,
後の設計インスペクションをやり易くする。
Copyright © 1994 Carnegie Mellon University7
設計検証を使う - 1
設計検証手法は次の期間に使うべきである
•設計中
•設計レビュー中
•設計インスペクション中
設計検証手法においては、テスト中に最もトラブルを引
き起こした欠陥タイプに、焦点を当てるべきである。
Copyright © 1994 Carnegie Mellon University8
設計検証を使う- 2
この講義と次の講義では、最も悩ませた設計欠陥の次
の範疇を説明する：
•状態機械の構造
•ループの構成体
もし時間が許せば、次の欠陥タイプに対して追加の検
証手法を適用する：
•ポインタ
•インタフェース
Copyright © 1994 Carnegie Mellon University9
設計検証のトピックス
次の２講義でカバーされた設計検証のトピックスは
•状態機械の正しさを検証すること
•実行表
•帰納法による証明
•トレース表
•数学的プログラムの検証
Copyright © 1994 Carnegie Mellon University10
状態機械の正しさ
計算システムの状態を変更する任意のプログラムは状
態機械である。
もしプログラムが同一の入力で異なる動作が出来れば
、このプログラムは状態機械である。
単純に見える状態機械が複雑な動作をすることがあり
得る。したがって状態機械を注意深く検証することが重
要である。
Copyright © 1994 Carnegie Mellon University11
状態機械の検証
状態機械が正しいことの検証の手順は次である：
•状態機械が隠れた落とし穴またはループをもたない
ことを保証するためのチェック
•全ての状態の集合が完全で直交していることのチェ
ック
•あらゆる状態からの全ての遷移（の集合）は完全で
直交していることのチェック
状態機械の正しさを検証した後、そのプログラムが意
図していたアプリケーション機能を実行することを保証
しなさい。
Copyright © 1994 Carnegie Mellon University12
隠れた落とし穴やループ - 1
隠れた落とし穴やループをチェックするために
•状態テンプレートを構築する
•状態機械ダイアグラムを構築する
•任意の出口状態が任意の他の状態から到達不可能
かを見極めよ
もし任意の出口状態が任意の他の状態から到達不可
能ならば、正規の(完全直交)状態機械ではない。
Copyright © 1994 Carnegie Mellon University13
隠れた落とし穴やループ - 2
例:次のようなオブジェクトＢＳｅｔを考えよう
•2 状態: EmptyState, MemberState
•4 メソッド: Push, Pop, Add, Subtract
•Pushは1つのメンバーをＢＳｅｔに加える
•PopはＢＳｅｔから１つのメンバーを取り除く
•AddはもしＢＳｅｔがすでに同じメンバーを含んでいな
ければメンバーをＢＳｅｔに加える。
•SubtractはもしＢＳｅｔが同一のメンバーを含んでい
ればＢＳｅｔからメンバーを取り除く。
Copyright © 1994 Carnegie Mellon University14
隠れた落とし穴やループ- 3
BSetに対する状態テンプレートは次のようになる：
EmptyState
n=0
EmptyState
Pop or Subtract
MemberState
Push or Add
MemberState
n >= 1
EmptyState
Pop(n=1) or Subtract(n=1)(D in BSet)
MemberState
Add or Push or Pop(n>1) or
Subtract(D not in BSet) or
Subtract(n>1)
Copyright © 1994 Carnegie Mellon University15
隠れた落とし穴やループ- 4
Pop or Subtract
EmptyState
n=0
Push or Add
MemberState
n>0
Pop(n=1) or
Subtract(n=1)(D in BSet)
Add or Push or Pop(n>1) or
Subtract(D not in BSet) or
Subtract(n>1)
Copyright © 1994 Carnegie Mellon University16
隠れた落とし穴やループ- 5
したがってこの状態機械が隠れた落とし穴あるいは
ループを持たないことは明らかである。
Copyright © 1994 Carnegie Mellon University17
全ての可能な状態- 1
よく起こる問題はある状態機械の状態を見落とすことで
ある。
初期状態、空状態、エラー状態等などがその例である。
状態パラメータの全ての可能な条件を確かめて、それら
の条件が含まれているかあるいは真に不可能かのいず
れかであることを保証しなさい。
Copyright © 1994 Carnegie Mellon University18
全ての可能な状態- 2
BSetをチェックする例:
•EmptyState は n = 0 である
•MemberState は n > 0 である
•n < 0 ではないので, これで全ケースをカバーする。
ｎ>0状態のどれも異なるべきでないことを保証するた
め, それらの状態のどれかが他の状態とは違った作動
を示すかどうかをチェックしなさい。
状態テンプレートまたは状態ダイアグラムをチェックす
ると全ての n>0 状態が同一の作動をすることが分か
る。したがってさらに状態を追加することは不要である
。
Copyright © 1994 Carnegie Mellon University19
状態の直交性
状態が直交しているためには、状態機械は一度に2つ
の状態が可能であってはならない。
先の状態機械においては,
n = 0 または n > 0 の何れかである.
状態は直交している、なぜならばその機械が
EmptyState (n = 0) あるいは MemberState (n >
0)の何れかでなければならないから; すなわち一度に
両方成り立つたつことはありえない。
Copyright © 1994 Carnegie Mellon University20
状態遷移 - 1
正規の(完全直交)状態機械では, 状態遷移はすべて
完全で直交していなければならない。
これが成り立つためには
•あらゆる状態はあらゆる可能なインプットに対して、
次の状態が定義されていなければならない。
•あらゆる状態はあらゆる可能なインプットに対して、
唯一の次の状態をもたなければならない。
Copyright © 1994 Carnegie Mellon University21
状態遷移 - 2
第1に、ＢＳｅｔ例のEmptyStateの完全性をチェックせ
よ：
•条件は Push, Pop, Add, および Subtractである。
•状態は各条件に対して定義されている、それゆえ
EmptyStateの遷移は完全である。
次の表は各条件が完全なことを示している：
Push
MemberState
Pop
EmptyState
Add
MemberState
Subtract
EmptyState
Copyright © 1994 Carnegie Mellon University22
状態遷移 - 3
次に、EmptyState の遷移が直交していることをチェッ
クしなさい。
EmptyStateへの遷移条件は Pop と Subtractである
.
MemberStateへの遷移条件は Push と Add である。
これらの次の状態遷移条件がオーバーラップしないの
で、その遷移条件は直交している。
Copyright © 1994 Carnegie Mellon University23
状態遷移 - 4
MemberStateの完全性に対して,可能なケースは表の
ようになる
D in BSet
n=1
n>1
D not in BSet
n=1
n>1
Push
Pop
MemberState
MemberState
MemberState
MemberState
EmptyState
MemberState
EmptyState
MemberState
Add
MemberState
MemberState
MemberState
MemberState
EmptyState
MemberState
MemberState
MemberState
Subtract
これらはすべて可能なケースであるので,
MemberStateの遷移は完全である。
Copyright © 1994 Carnegie Mellon University24
状態遷移 - 5
MemberStateの直交性について, 遷移の間にオーバ
ーラップがあってはならない。
•MemberStateから EmptyStateへの遷移は
Pop(n=1) or Subtract(n=1)and (D in BSet)の時
に起こる。
•MemberStateから MemberStateへの遷移は Add
+ Push + Pop(n>1) + Subtract(D not in BSet) +
Subtract(n>1)の時に起こる。
前の図から明らかなように、これらの二つのケースは
共通に持つ条件はないので直交している。
Copyright © 1994 Carnegie Mellon University25
演習- 1
SignOnのオブジェクトは次のメソッドをもつものとする
。
•Open ーsign-on手続きを開始する。
•LogOn ー名前を要求する
•もしその名前が正しければ、PassWordがパスワー
ドを要求する
•もしPassWordが正しければ, SignOnは値“真”を
以って終了する。
•もし何かエラーがあれば, そのプログラムはもう一度
LogOnから始める。
•エラーが２回起これば SignOnは値“偽”を以って終
了する。
Copyright © 1994 Carnegie Mellon University26
演習 - 状態ダイアグラム
StandBy
Open
Start
LogOn(No)
Error
LogOn(Yes)
NameOk
PassWord(Yes)
(true)
LogOn(No)
(false)
PassWord(No)
LogOn(Yes)
Trial
PassWord(Yes) (true)
PassWord(No) (false)
Copyright © 1994 Carnegie Mellon University27
演習- 2
SignOn状態テンプレートと状態ダイアグラムを構築し
なさい。
隠された落とし穴とループをチェックしなさい。
状態の完全性と直交性をチェックしなさい。
遷移の完全性と直交性をチェックしなさい。
Copyright © 1994 Carnegie Mellon University28
演習-状態仕様テンプレート
StandBy
n=0
Start
Open
Start
NameOk
Error
NameOk
Error
StandBy (true)
Error
Trial
StandBy (false)
Trial
StandBy (true)
StandBy(false)
n=1
LogOn(Yes)
LogOn(No)
n=2
PassWord(No)
Password(Yes)
n=3
LogOn(Yes)
LogOn(No)
n=4
PassWord(Yes)
PassWord(No)
Copyright © 1994 Carnegie Mellon University29
実行表- 1
実行表はプログラムの実行を追跡するきちんとした方
法である。
•プログラムフローの手によるチェックである。
•初期条件でスタートする。
•変数の値の集合が選択される。
•各実行ステップが調べられる。
•変数値の全ての変更が記入される。
•プログラムの動作は仕様に対してチェックされる。
Copyright © 1994 Carnegie Mellon University30
実行表- 2
実行表の長所は以下である。
•単純である。
•証明の結果が信頼できる
実行表の短所は以下である。
•一度に1ケースしかチェックできない。
•時間がかかる
•人間エラーの影響を受ける
Copyright © 1994 Carnegie Mellon University31
実行表の手順
実行表を使用するために
•キープログラム変数を認識し、トレース表のトップに
それらを記入する。
•主要なプログラムステップを記入する。
•初期条件を決定し記入する。
•変数の値を各プログラムステップを通じて追跡する。
•ループの反復に対しては、追加のループサイクルの
各々に対して、追加の実行表ステップを加える。
•長いループに対しては, もしそれらの結果が明らかで
あるならば、中間ステップをｸﾞﾙｰﾌﾟにせよ。
Copyright © 1994 Carnegie Mellon University32
実行表の例- 1
Cycle 1
#
ClearSpaces(var Input: string; State: int)
命令
条件
‘ AB ‘
1 Length = length(Input)
2 if Length > 0
Input
Length State
5
0
true
3 repeat(until State=3 or Length=0)
4
if Input[Length-1] = ‘ ‘
5
Length = Length - 1
6
if State < 2 State=State+1
true
4
true
1
7 else State = 3
until State=3 or Length=0
false
Copyright © 1994 Carnegie Mellon University33
実行表の例- 2
until条件が満足される前に3つのｻｲｸﾙが要求される
ﾃｽﾄｹｰｽとちょうど同様に、実行表はこの特定の変数
の組み合わせに対するケースのみを証明する。
初期条件を、それらがﾌﾟﾛｸﾞﾗﾑによってセットされること
を保証するため、注意深くチェックしなさい。
エラーともれに対して実行表を２重にチェックしなさい。
Copyright © 1994 Carnegie Mellon University34
帰納法による証明
この方法は整数パラメータをもつブール関数に適用す
る。
このことは以下を述べている。
もし n = ｋに対してf（n）が“真”で
かつもし
• n = z ただし z > k
• かつ f(z) が真のとき
•f(z+1) が真であることを示すことができる
ならこのとき、kより大きい全てのｎに対して f(n) が真
である
Copyright © 1994 Carnegie Mellon University35
帰納法による証明の例
例:
for i=1 to Limit
do xyz
もし
•このことがＬｉｍｉｔ = １に対して真であることを示す
ことができ、かつ
•ある任意のより大きな値ｚに対して真であり、かつ
•そのときｚ+１に対しても真であることを示すことが
出来るなら、
•そのときＬｉｍｉｔのすべての正の値に対して真であ
る
Copyright © 1994 Carnegie Mellon University36
帰納法による証明の技法
もし
•あなたが変数ｘを使用する設計要素をもっている
•その要素が x= ｋに対して働くことを検証する
次に
•あるより大きな値 x = ｚに対して働くと仮定する
•ﾌﾟﾛｸﾞﾗﾑの作動がｚ＋１で不適当になる z の値を見
つけるよう試みる
もしあなたが出来なければ、証明は完了する。
Copyright © 1994 Carnegie Mellon University37
階乗の例 - 1
次のﾌﾟﾛｸﾞﾗﾑがN!を計算することを証明しなさい。
Factorial(N)
F=1
for i = 1 to N
F = F*i
return = F
Copyright © 1994 Carnegie Mellon University38
階乗の例 - 2
k = 1 とする、そして N=1のとき, F = N!であることを証
明する。
•１の階乗は１であるので、これは正しい。
次に, N = z のとき, F = z!が成り立つと仮定する。
最後に, F(z) = z! でかつ F(z+1) <> (z+1)!である
ｚの任意の値を見つけよう。
この様なｹｰｽは次の時のみ起こるであろう
•数を計算するｼｽﾃﾑが限界値を超えてしまった時
•計算能力を超えてしまった時
Copyright © 1994 Carnegie Mellon University39
演習問題 #12
ﾃｷｽﾄの第１２章を読みなさい。
ﾌﾟﾛｸﾞﾗﾑ１０A の開発を続ける.
もし時間があれば, 最終報告R5の作業を始めなさい。
R5の仕様書は付録Dで見つけることが出来る。
Copyright © 1994 Carnegie Mellon University40
講義12で覚えておくべきメッセージ
1. もしあなたが設計ﾚﾋﾞｭｰ手法規範を使えば、
あなたの設計ﾚﾋﾞｭｰによる欠陥摘出率は顕著に
改善するだろう。
2. 設計の検証に消費する時間はﾃｽﾄ時間の節約によ
って十二分におつりがでるであろう。
3. 検証技法をいくつか練習しそして、あなたがﾃｽﾄの
際にもっともよく発見する欠陥を発見するのに
もっとも効果的なものを、その中から選択する。
Copyright © 1994 Carnegie Mellon University41

Download Report