• 検索結果がありません。

仕様記述フレームワークの基本型

ドキュメント内 九州大学学術情報リポジトリ (ページ 96-101)

第 5 章 レビューとテストの用途を考慮した仕様記述フレームワークの提案 79

5.1.2 仕様記述フレームワークの基本型

86 第 5 章 レビューとテストの用途を考慮した仕様記述フレームワークの提案

図5.3 Action Selection 部とAction Requirement 部の構成例

Requirement部と呼ぶこととする.

次の5.1.2節では仕様記述フレームワークの基本型について述べる. 仕様記述フレーム

ワークの基本型とは, Action Selection 部内では条件の判定のみを行い, 条件判定中に入 力データや内部状態を変更する必要がない簡単な仕様記述の構造である. その次の5.1.3

節ではAction Selection 部内で入力データや内部状態を変更しながら条件判定を行う必

要がある仕様記述フレームワークの拡張型を提案する. これは, 5.1.1節のディシジョン テーブルを作成する上での注意事項として述べた, 条件間に依存関係がある場合に用い る仕様記述フレームワークである. 例えば, 暗号化したデータを入力とする場合, 暗号化 データの復号に関する Action Selection 部の条件記述と, 入力データを復号処理した後 に,復号した入力データに関する条件を記述したAction Selection部が必要になる. この

ように, Action Selection 部内で処理が必要な仕組みを仕様記述フレームワークの拡張型

と呼ぶこととする.

5.1. ラベル付き条件による仕様記述フレームワークの提案 87 表5.2 図5.4の仕様記述をディシジョンテーブルで表した例

ルール

条件 1 2 3 4

ConditionA N Y Y Y ConditionB - N Y Y ConditionC - - N Y アクション

Act1Requirement Y N N N Act2Requirement N Y Y N Act3Requirement N N N Y

結果の事後条件を記述する.

図5.3 の例をVDM++ により記述した例を図5.4に示す. Specification 関数は図5.2 において示した,宣言的な記述箇所に対応する仕様伝達部である. すなわち,「入力」と

「入力時の内部状態」である,「 in : INPUT 」と「state in : STATE 」, 並びに, 「出 力」と「出力時の内部状態」である,「 out : OUT 」と「 state out : STATE 」を用い て仕様を宣言的に記述することができる.

Specification 関数内のcases式において, ActionSelection関数を呼び出し,この関数の 結果から, Act1Requirement関数, Act2Requirement関数, Act3Requirement関数を選択

する. Specification関数は,ディシジョンテーブルの条件の組み合わせとアクションの関

係を記述したものであり, ActionSelection 関数は, ディシジョンテーブルの条件の組み 合わせを記述したものである. 図5.4 に対応するディシジョンテーブルを表5.2に示す. 例えば, ディシジョンテーブルのルール 1 から, ConditionA 関数が「 N 」つまり false である場合, Act1Requirement 関数が選択されることが分かる.

図5.4に示した ActionSelection 関数の内部は, cases 式と条件群からなる簡潔な構造 となっている. 簡潔性を保つために以下のようなコーディングガイドラインを定めてい る. まず, VDM++ の言語仕様から cases 式の構文例を図5.5に示す.

「 e 」 は1 つの任意の式であり, 「 pij 」は1 つ 1つが式 e にマッチするパターン

である. VDM++ の言語仕様上, 「 pij 」のパターンの列をパターンリストと呼ぶ. 上

88 第 5 章 レビューとテストの用途を考慮した仕様記述フレームワークの提案

Specification : INPUT * STATE * OUT * STATE -> bool Specification (in, state_in, out, state_out) ==

cases ActionSelection (in, state_in) :

<ACTION1> ->

Act1Requirement (in, state_in, out, state_out),

<ACTION2> ->

Act2Requirement (in, state_in, out, state_out),

<ACTION3> ->

Act3Requirement (in, state_in, out, state_out), others ->

false end;

ActionSelection : INPUT * STATE -> SELECTION_RESULT ActionSelection (in, state_in) ==

cases false :

(ConditionA (in, state_in)) ->

<ACTION1>,

(ConditionB (in, state_in)), (ConditionC (in, state_in)) ->

<ACTION2>, others ->

<ACTION3>

end;

図5.4 基本型の VDM++ による記述例

九州大学大学院 システム情報科学府 情報工学専攻

5.1. ラベル付き条件による仕様記述フレームワークの提案 89

cases e :

p11, p12, ..., p1k -> e1, p21, p22, ..., p2l -> e2, ...

pn1, pn2, ..., pnm -> en,

others -> enplus1

end;

図5.5 cases 式の構文例

記の例において, i は 1 からn となり, j は 1から k, l, m を用いて表した範囲の値であ る. k, l, m, n は 1 以上の整数である. 「 ei 」で表すのは任意の式である. 「 pij 」で 表すパターンが e にマッチした場合「 ei 」が呼ばれる. 「 others 」とそれに対応する

式「enplus1 」はオプションである. 「 others 」は,いずれのパターンも e にマッチし

なかった場合, 「 enplus1」が呼ばれることを表している. 次に, 本研究において定めた コーディングガイドラインを以下に示す.

「cases e :」の eはfalse値とする. つまり,「cases false :」とする. パターンリス ト中のいずれかのパターンがfalseであった場合に「 ei」が呼び出される. パター ンリスト中の全てパターンが true であった場合は「others 」となり「 enplus1」 が呼び出される.

「 pij 」はtrue またはfalseを返す関数呼び出しにより構成することとする. 例え

ば,図5.4のConditionA関数, ConditionB関数, ConditionC関数のように,「pij」 は関数呼び出しとする.

この構成により, ディシジョンテーブルで表した条件の組み合わせとアクションの関 係を, 簡潔な構造を用いて VDM++ により記述することができた. 本研究では, この ConditionA 関数といったture またはfalse を返す「pij」のパターンリスト内の関数を

90 第 5 章 レビューとテストの用途を考慮した仕様記述フレームワークの提案

ラベル付き条件と呼び, パターンリストに列挙したラベル付き条件の集合をラベル付き 条件群と呼ぶこととする.

以下では, このcases 式を用いた記述について考察する. cases式により, ディシジョン

テーブルに対応する仕様を, 簡潔な構造で表現することができた. しかし, VDM++ の 言語仕様上, パターンリスト中の「 pij 」の評価順序は規定されていないことに注意す る必要がある. そのため, パターンリスト中の「 pij 」の中で複数の「 pij 」が false と なった場合, どの「 ei 」が選択されるのかは未定義となる. 本来, 「 cases e :」を false とした場合, 「 pij 」中で常に 1 つだけが false となるように, 「 pij 」を互いに素の関 係にすることが一般的である. しかし,本フレームワークにおいて, 互いに素の関係とな るように厳密に記述した場合, 記述が複雑になってしまうという課題があった. 例えば, 表5.2のディシジョンテーブルのルール 1 において, ConditionA 関数が「 N 」つまり false の場合, ConditionB 関数と ConditionC 関数は「」として, 条件判定の対象外で あることを表している. つまり, ConditionA 関数が false であった場合, ConditionB 関 数と ConditionC 関数の判定結果にかかわらず, ConditionA 関数が false の場合のアク ションを選択することを表している. しかし,図5.4のVDM++ の記述例では,言語仕様 上は, ConditionA 関数と ConditionB 関数と ConditionC 関数の評価順序は規定してい ない. これは,上記のとおりcases 式は「pij 」の評価順序を規定していないからである.

そのため, ConditionA 関数が false であったとしても, ConditionB 関数と ConditionC 関数の結果がfalse であった場合, ConditionA関数がfalseの場合のアクションが選択さ れるとは限らないこととなる. 現時点は, VDMToolsのインタープリタ機能が,パターン リストの先頭から順に評価を行っているため,「 pij 」の中で先に false となった「ei 」 を呼び出している. VDM++ の言語仕様上は, 本フレームワークの使い方は問題ではあ るが, 現在は,このインタープリタ機能の判定順序を仕様として, このディシジョンテー ブルの「」の仕様を表現している. これは, VDM++ の構文を使って, 「」の仕様を 簡潔に表現することは難しいためである. VDM++の言語仕様の検討も含めて今後の課 題としたい.

九州大学大学院 システム情報科学府 情報工学専攻

5.1. ラベル付き条件による仕様記述フレームワークの提案 91

図5.6 拡張型のフレームワークの例

ドキュメント内 九州大学学術情報リポジトリ (ページ 96-101)