Disciplined Software Engineering Lecture #12 コメントは特にありません。 ---------- ページ3, 35, 36, と41に若干手を加えましたが，変更は本質的ではありません。 （久保記，1999.2.28) Software Engineering Institute Carnegie Mellon University Pittsburgh, PA 15213 Sponsored by the U.S. Department of Defense

設計検証 設計検証は2つの講義でカバーされる。この講義では以下を述べる。 設計検証する理由 状態機械の正しさ 実行表 帰納法による証明 次の講義は以下をカバーする トレース表 数学的プログラムの検証 プログラムの証明

設計検証の必要性- 1 あなたのＰＳＰを改善するために作業するのにしたがって、あなたは設計の欠陥数を顕著に減少させることは難しいと思うようになるだろう。 チェックリストを使い、注意力を増やすことによってあなたのコードレビューによる欠陥摘出率を改善できる。 設計レビューによる欠陥摘出率を改善するために、あなたは検証手法規範を使うことが必要になる。 「規律ある検証手法」を「検証手法規範」に変更しました。（久保，1999.1.28)

設計検証の必要性- 2 設計検証に対するきちんとしたアプローチが本質的である。なぜならば 多くのよくある設計欠陥は条件が見落とされることによって引き起こされる ありそうもない状況のように見えることが強力な計算システムにおいて起こりやすくなっている 最初のプログラムバージョンでは起こり得なかった条件が後の修正によって引き起こされるかもしれない。

設計検証の必要性- 3 構造化された設計検証の手続きに従うことによって、以下の可能性が増える 見落とされた条件に気がつく まれにしか露出しないリスクを確認する 将来起こりうる危険を認識する 設計レビューに関するデータを記録することによって, 後の設計インスペクションをやり易くする。

設計検証を使う - 1 設計検証手法は次の期間に使うべきである 設計中 設計レビュー中 設計インスペクション中 あなたの設計検証手法はテスト中にあなたに最もトラブルを引き起こした欠陥タイプに焦点を当てるべきである。

設計検証を使う- 2 この講義と次の講義では私を最も悩ませた設計欠陥カテゴリーに言及するつぎの話題を選択した。 状態機械の構造 ループの構成体 もし利用可能であれば私は次のような欠陥タイプに対して追加の検証手法を使うつもりである ポインタ インタフェース

設計検証のトピックス 次の２講義でカバーされた設計検証のトピックスは 状態機械の正しさを検証すること 実行表 帰納法による証明 トレース表 数学的プログラムの検証

状態機械の正しさ 計算システムの状態を変更する任意のプログラムは状態機械である。 もしプログラムが同一の入力で異なる動作が出来れば、このプログラムは状態機械である。 単純に見える状態機械が複雑な動作をすることがあり得る。したがって状態機械を注意深く検証することが重要である。

状態機械の検証 状態機械の検証におけるステップは次である 状態機械が隠れた落とし穴またはループをもたないことを保証するためのチェック 全ての状態の集合が完全で直交していることのチェック あらゆる状態からの全ての遷移の集合は完全で直交していることのチェック 状態機械の正しさを検証した後、そのプログラムが意図していたアプリケーション機能を実行することを保証しなさい。

隠れた落とし穴やループ - 1 隠れた落とし穴やループをチェックするために 状態テンプレートを構築する 状態機械ダイアグラムを構築する 任意の出口状態が任意の他の状態から到達不可能かを決定する もし任意の出口状態が任意の他の状態から到達不可能ならばこれは正規の(完全直交)状態機械ではない。

隠れた落とし穴やループ - 2 例:次のようなオブジェクトＢＳｅｔを考えよう 2 状態: EmptyState, MemberState 4 メソッド: Push, Pop, Add, Subtract Pushは1つのメンバーをＢＳｅｔに加える PopはＢＳｅｔから１つのメンバーを取り除く AddはもしＢＳｅｔがすでに同じメンバーを含んでいなければメンバーをＢＳｅｔに加える。 SubtractはもしＢＳｅｔが同一のメンバーを含んでいればＢＳｅｔからメンバーを取り除く。

隠れた落とし穴やループ- 3 BSetに対する状態テンプレートは次のようになる： n >= 1 EmptyState n = 0 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)

隠れた落とし穴やループ- 4 Pop or Subtract EmptyState n = 0 Push or Add Pop(n=1) or Subtract(n=1)(D in BSet) MemberState n > 0 Add or Push or Pop(n>1) or Subtract(D not in BSet) or Subtract(n>1)

隠れた落とし穴やループ- 5 したがってこの状態機械が隠れた落とし穴あるいはループを持たないことは明らかである。

全ての可能な状態- 1 よく起こる問題はある状態機械の状態を見落とすことである。 初期状態、空状態、エラー状態等などがその例である。 状態パラメータの全ての可能な条件を確かめて、それらの条件が含まれているかあるいは真に不可能かのいずれかであることを保証しなさい。

全ての可能な状態- 2 BSetをチェックする例: EmptyState は n = 0 をもつ MemberState は n > 0 をもつ n < 0 ではないので, これで全ケースをカバーする。 ｎ>0状態のどれも異なるべきでないことを保証するため, それらの状態のどれかが他の状態とは違った作動を示すかどうかをチェックしなさい。 状態テンプレートまたは状態ダイアグラムをチェックすると全ての n>0 状態が同一の作動をすることが分かる。したがってさらに状態を追加することは不要である。

状態の直交性 状態が直交しているべきためには、状態機械は一度に2つの状態が可能であってはならない。 例の状態機械においては, n = 0 または n > 0 の何れかである. 状態は直交している、なぜならばその機械が EmptyState (n = 0) あるいは MemberState (n > 0)の何れかでなければならないから; すなわち一度に両方成り立つたつことはありえない。

状態遷移 - 1 正規の(完全直交)状態機械では, 状態遷移はすべて完全で直交していなければならない。 これが成り立つためには あらゆる状態はあらゆる可能なインプットに対して、 次の状態が定義されていなければならない。 あらゆる状態はあらゆる可能なインプットに対して、唯一の次の状態をもたなければならない。

状態遷移 - 2 第1に、ＢＳｅｔ例のEmptyStateの完全性をチェックせよ： 条件は Push, Pop, Add, および Subtractである。 状態は各条件に対して定義されている、それゆえ EmptyStateの遷移は完全である。 次の表は各条件が完全なことを示している： Push MemberState Pop EmptyState Add MemberState Subtract EmptyState

状態遷移 - 3 次に、EmptyState の遷移が直交していることをチェックしなさい。 EmptyStateへの遷移条件は Pop と Subtractである. MemberStateへの遷移条件は Push と Add である。 これらの次の状態遷移条件がオーバーラップしないので、その遷移条件は直交している。

状態遷移 - 4 MemberStateの完全性に対して,可能なケースは表のようになる これらはすべて可能なケースであるので, D in BSet D not in BSet n = 1 n > 1 Push Pop Add Subtract MemberState EmptyState これらはすべて可能なケースであるので, MemberStateの遷移は完全である。

状態遷移 - 5 MemberStateの直交性に対して, 遷移の間にオーバーラップがあってはならない。 MemberStateから EmptyStateへの遷移は Pop(n=1) あるいは Subtract(n=1) かつ (D in BSet)の時に起こる。 MemberStateから MemberStateへの遷移は Add + Push + Pop(n>1) + Subtract(D not in BSet) + Subtract(n>1)の時に起こる。 前の図から明らかなように、これらの二つのケースは 共通に持つ条件はないので直交している。

クラスの演習- 1 SignOnのオブジェクトは次のメソッドをもつものとする。 Open ーsign-on手続きを開始する。 LogOn ー名前を要求する もしその名前が正しければ、PassWordがパスワードを要求する もしPassWordが正しければ, SignOnは値“真”を以って終了する。 もし何かエラーがあれば, そのプログラムは もう一度LogOnから始める。 エラーが２回起これば SignOnは値“偽”を以って終了する。

クラスの演習- 2 SignOn状態テンプレートと状態ダイアグラムを構築しなさい。 隠された落とし穴とループをチェックしなさい。 状態の完全性と直交性をチェックしなさい。 遷移の完全性と直交性をチェックしなさい。

クラスの演習 - 状態ダイアグラム StandBy LogOn(No) Open (false) LogOn(No) Start Error LogOn(Yes) LogOn(Yes) NameOk PassWord(No) Trial PassWord(Yes) (true) PassWord(Yes) (true) PassWord(No) (false)

演習-状態テンプレート StandBy n = 0 Start Open Start n = 1 NameOk LogOn(Yes) Error LogOn(No) NameOk n = 2 Error PassWord(No) StandBy (true) Password(Yes) Error n = 3 Trial LogOn(Yes) StandBy (false) LogOn(No) Trial n = 4 StandBy (true) PassWord(Yes) StandBy(false) PassWord(No)

実行表- 1 実行表はプログラムの実行を追跡するきちんとした方法である。 プログラムフローの手によるチェックである。 初期条件でスタートする。 変数の値の集合が選択される。 各実行ステップが調べられる。 変数値の全ての変更が記入される。 プログラムの動作は仕様に対してチェックされる。

実行表- 2 実行表の長所は以下である。 単純である。 証明の結果が信頼できる 実行表の短所は以下である。 一度に1ケースしかチェックできない。 時間がかかる 人間エラーの影響を受ける

実行表の手順 実行表を使用するために キープログラム変数を認識し、トレース表のトップにそれらを記入する。 主要なプログラムステップを記入する。 初期条件を決定し記入する。 変数の値を各プログラムステップを通じて追跡する。 ループの反復に対しては、追加のループサイクルの各々に対して、追加の実行表ステップを加える。 長いループに対しては, もしそれらの結果が明らかであるならば、中間ステップをｸﾞﾙｰﾌﾟにせよ。

実行表の例- 1 Cycle 1 ClearSpaces(var Input: string; State: int) # 命令 条件 Length State 1 Length = length(Input) ‘ AB ‘ 5 2 if Length > 0 true 3 repeat(until State=3 or Length=0) 4 if Input[Length-1] = ‘ ‘ true 5 Length = Length - 1 4 6 if State < 2 State=State+1 true 1 7 else State = 3 until State=3 or Length=0 false

実行表の例- 2 until条件が満足される前に3つのｻｲｸﾙが要求される ﾃｽﾄｹｰｽとちょうど同様に、実行表はこの特定の変数の組み合わせに対するケースのみを証明する。 初期条件を、それらがﾌﾟﾛｸﾞﾗﾑによってセットされることを保証するため、注意深くチェックしなさい。 エラーともれに対して実行表を２重にチェックしなさい。

帰納法による証明 この方法は整数パラメータをもつブール関数に適用する。 このことは以下を述べている。 もし n = ｋに対してf（n）が“真”で かつ もし n = z ただし z > k かつ f(z) が 真のとき f(z+1) が真であることを示すことができる ならこのとき、kより大きい全てのｎに対して f(n) が真である 少し手をいれました。 英文には違和感があります。n=z で n を持ち込むなら f(z), f(z+1)ではなく f(n), f(n+1)を使うのがいい。それか n を持ち込まないで z だけですますか。(久保，1999.1.28)

帰納法による証明の例 例: for i=1 to Limit do xyz もし このことがＬｉｍｉｔ = １に対して真であることを示す　ことができ、かつ ある任意のより大きな値ｚに対して真であり、かつ そのときｚ+１に対しても真であることを示すことが出来るなら、 そのときＬｉｍｉｔのすべての正の値に対して真である 日本語をすこし変えて厳密にしました。(久保記，1999.1.28)

帰納法による証明の技法 もし あなたが変数 ｘ を使用する設計要素をもっている その要素が x= ｋ に対して働くことを検証する 次に ﾌﾟﾛｸﾞﾗﾑの作動が ｚ＋１ で不適当になる z の値を見つけるよう試みる もしあなたが出来なければ、証明は完了する。

階乗の例 - 1 次のﾌﾟﾛｸﾞﾗﾑがN!を計算することを証明しなさい。 Factorial(N) F = 1 for i = 1 to N F = F*i return = F

階乗の例 - 2 k = 1 とする、そして N=1のとき, F = N!であることを証明する。 １の階乗は １ であるので、これは正しい。 次に, N = z のとき, F = z!が成り立つと仮定する。 最後に, F(z) = z! でかつ F(z+1) <> (z+1)!である ｚ の 任意の値を見つけよう。 この様なｹｰｽは次の時のみ起こるであろう 数を計算するｼｽﾃﾑが限界値を超えてしまった時 計算能力を超えてしまった時

演習問題 #12 ﾃｷｽﾄの第１２章を読みなさい。 ﾌﾟﾛｸﾞﾗﾑ １０A の開発を続ける. もし時間があれば, 最終報告R5の作業を始めなさい。 R5の仕様書は付録Dで見つけることが出来る。

講義12で覚えておくべきメッセージ 1. もしあなたが設計ﾚﾋﾞｭｰ手法規範を使えば、 あなたの設計ﾚﾋﾞｭｰによる欠陥摘出率は顕著に 1. もしあなたが設計ﾚﾋﾞｭｰ手法規範を使えば、 あなたの設計ﾚﾋﾞｭｰによる欠陥摘出率は顕著に 　　改善するだろう。 2. 設計の検証に消費する時間はﾃｽﾄ時間の節約によ って十二分におつりがでるであろう。 3. 検証技法をいくつか練習しそして、あなたがﾃｽﾄの 際にもっ ともよく発見する欠陥を発見するのに もっとも効果的なものを、その中から選択する。 「訓練された設計ﾚﾋﾞｭｰ手法」は「設計ﾚﾋﾞｭｰ手法規範」に変更しました。3.に「いくつか」と「その中から」を挿入しました。（久保記，1999.1.28)