本提案手法を用いた具体的な記述例による評価

62 第 4 章 仕様と設計を分離する実行可能仕様の設計・構成法の提案

型を隠蔽するために, 以下のような型の仕様記述のルールを定めた. まず,型を 2つに 分類した. 仕様で定義する「仕様の型」と,仕様では定義しない「隠蔽対象の型」である.

「仕様の型」とは, 工程が仕様策定と設計工程とに分かれる中で, 仕様策定者が仕様とし て規定する型である. そのため, 設計者はこの型の定義に従うべき型である. この型は, 仕様策定者の責任範囲とする型である. 一方,「隠蔽対象の型」とは, 設計に自由度を持 たせるために, 仕様策定者が仕様策定工程では規定しない型である. この型は, 設計工程 で設計者の責任範囲として規定すべき型である. 次に,「隠蔽対象の型」の定義・演算子 を隠蔽するための関数を導入した. この関数を「隠蔽関数」と呼ぶこととする. 図4.4の 仕様伝達部から「隠蔽対象の型」の値を使用する場合は, 必ず「隠蔽関数」を経由する ルールとした. このルールにより,「隠蔽対象の型」の型の定義と型演算子を仕様伝達部 から直接参照する記述を排除することができた. また, 「仕様の型」と「隠蔽対象の型」

を区別する型の命名ルールを定めることで, 設計者をはじめとする仕様記述の読み手が

「仕様の型」と「隠蔽対象の型」を区別できるようにした. 4.3 節において, 具体的な記 述例を用いて説明し, 提案手法の評価を行う.

4.3. 本提案手法を用いた具体的な記述例による評価 63

と示す.

2 つ目の評価は, 4.2節において述べた, 仕様と設計の分離に関する課題を解決する形 式仕様記述の設計・構成法の提案に関する評価である. 評価において,提案の手法を用い た場合と, 用いなかった場合の記述例を比較し, 本提案手法の有効性を示す.

以降の本節では,具体例として,図4.6 に示したアドレス帳の例を用いる. この記述例 の詳細は, 各節の中で述べる.

4.3.1 「実行可能性の影響」を解決する仕様記述スタイルの評価

まず, 図4.6に示した具体例について, 「新規カード登録」関数を例に, 「実行可能性 の影響」の課題を解決する仕様記述スタイルについて議論する. 「新規カード登録」関 数を次に示す.

public 新規カード登録 : BOOK * CARD -> BOOK 新規カード登録 (bk, cd) ==

impl_新規カード登録 (bk, cd)

pre cd.Name not in set 名前集合 (bk)

post カード集合 (RESULT) = カード集合 (bk) union {cd};

「新規カード登録」関数は, 引数としてアドレス帳を表す BOOK 型, および名前とアド レスからなる登録対象のCARD 型を受け取り,戻り値として登録後のBOOK 型を返す.

「新規カード登録」関数の事前条件 (pre) は次の条件式である. pre cd.Name not in set 名前集合 (bk)

これは,登録対象のカードが登録済みではないことを示している. 以降では,この事前条 件を「 pre 新規カード登録」と表記する. 事後条件 (post) は次の条件式である.

post カード集合 (RESULT) = カード集合 (bk) union {cd};

これは,次のように読むことができる. 登録後のアドレス帳のカード集合は,登録前のア ドレス帳のカード集合に, 登録対象のカードを加えたものとなっていること, という条件

64 第 4 章 仕様と設計を分離する実行可能仕様の設計・構成法の提案

types

public NAME = seq of char; -- ^仕様の型 public ADDRESS = seq of char; -- ^仕様の型

public CARD :: -- ^仕様の型

Name : NAME

Address : ADDRESS;

public BOOK = BOOK_IMPL; -- ^{隠蔽対象の型}

public BOOK_IMPL = map NAME to CARD; -- ^{非伝達部の型}

functions

-- 拡張陽関数定義による機能仕様の記述

public ^{新規カード登録} : BOOK * CARD -> BOOK 新規カード登録 (bk, cd) ==

impl_^{新規カード登録} (bk, cd) -- ^非伝達部 pre cd.Name not in set ^名前集合 (bk) -- ^{仕様伝達部} post ^{カード集合} (RESULT)

= ^{カード集合} (bk) union {cd}; -- ^{仕様伝達部}

-- ^{「隠蔽対象の型」}BOOK ^{の「隠蔽関数」}

public ^{カード集合} : BOOK -> set of CARD カード集合(bk) ==

rng bk;

public 名前集合 : BOOK -> set of NAME 名前集合(bk) ==

dom bk;

-- 新規カード登録の非伝達部

private impl_^{新規カード登録} : BOOK * CARD -> BOOK impl_新規カード登録 (bk, cd) ==

bk munion {cd.Name |-> cd}

図4.6 本研究において提案する方法を用いた仕様記述の例

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

4.3. 本提案手法を用いた具体的な記述例による評価 65

図4.7 「実行可能性の影響」を解決する仕様記述スタイルと仕様記述例との対応関係

式である. 以降では, この事後条件を「 post 新規カード登録」と表記する. 「新規カー ド登録」関数の関数本体は次の記述である.

impl_新規カード登録 (bk, cd)

以降では, この関数本体を「 impl 新規カード登録」と表記する.

「新規カード登録」関数は, 本研究において提案した図4.4の記述スタイルを用いた. 提案の記述スタイルと「新規カード登録」関数との対応関係を図4.7 に示す. 「入力」

は,「新規カード登録」関数の引数である「cd : CARD 」である. 図中では,関数内の該 当箇所を指し示すために「変数名 : 型」という表記を用いることとする. 「入力時の内 部状態」も関数の引数である「 bk : BOOK 」となる. 非伝達部は「 impl 新規カード登 録」となる. 非伝達部であることを明確にするために, implementation を表す「 impl 」 を関数の先頭に付ける命名ルールとした. 仕様伝達部は, 事前条件と事後条件の「 pre 新規カード登録」と「 post 新規カード登録」となる. 仕様伝達部では, 「出力」と「出 力時の内部状態」を使用して, 入出力の関係を宣言的に記述することができる.

66 第 4 章 仕様と設計を分離する実行可能仕様の設計・構成法の提案

以上から,「実行可能性の影響」を回避することができる. 「実行可能性の影響」とは

「解決すべき問題」である What を記述するべき仕様に,「問題の解決方法」である How の要素を多く含んだ記述が影響を及ぼし,設計者を過剰に制約し, 仕様が複雑になるとい うものであった. 宣言的な記述により,「問題の解決方法」であるHow の要素を含まな い仕様を記述することができる. また, 「動かすこと」を目的とした記述を, 図4.7 に示 した非伝達部にのみ記述し, 非伝達部のみから呼び出す関数には, implementation を表 す「 impl 」を関数名の先頭に付ける命名ルールとした. これにより,「動かすこと」を 目的にした記述と,「伝えること」を目的にした記述を区別し,理解容易性に優れた仕様 を記述することができることを示した.

次に, 仕様アニメーションによる動作検証時に課題となる,評価者の作業工数の課題に ついて,図4.4において提案した記述スタイルを用いて,この課題が解決できること示す.

まず, 図4.3の記述スタイルの場合に, VDM++ を用いたテストスクリプトの記述から, 評価者の作業工数が課題となる具体例を示す. 次に, 既に示した「新規カード登録」関数 と図4.7に関するテストスクリプトの記述から, この課題が解決できることを示す.

評価者の作業工数が課題となるケースは,図4.3 に示した宣言的な記述を行った場合で あった. この宣言的な記述スタイルは,前述の「新規カード登録」関数の事後条件「 post 新規カード登録」の記述に対応している. 対応関係を図4.8 に示す. 4.1.3節において述 べたように, 関数の事後条件は VDMTools のインタープリタ機能を使用して, 次のよう に呼び出すことができる.

post_新規カード登録 (bk, cd, result_bk)

ここで, bkは実行前のアドレス帳を表すBOOK型, cdは登録対象のカードを表すCARD

型, result bk は「新規カード登録」関数の戻り値のBOOK 型である. この「 post 新規

カード登録」関数に対するテストスクリプトの記述から, 評価者の作業工数が課題とな る具体例を示す.

VDM++ を用いて記述したテストスクリプトを示す. まず, 「 post 新規カード登録」

関数のテストを行うために, テスト対象のアドレス帳であるBOOK型を作成するための

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

4.3. 本提案手法を用いた具体的な記述例による評価 67

図4.8 宣言的な記述スタイルと仕様記述例との対応関係

関数は次のようになる.

public MakeAddressBook : () -> BOOK MakeAddressBook () ==

let

a = mk_CARD ("a", "[email protected]"), b = mk_CARD ("b", "[email protected]"), c = mk_CARD ("c", "[email protected]"), d = mk_CARD ("d", "[email protected]"), e = mk_CARD ("e", "[email protected]"), f = mk_CARD ("f", "[email protected]") in{

a.Name |-> a, b.Name |-> b, c.Name |-> c, d.Name |-> d, e.Name |-> e, f.Name |-> f };

68 第 4 章 仕様と設計を分離する実行可能仕様の設計・構成法の提案

MakeAddressBook 関数では, 名前が a から f で, アドレスが[email protected] から[email protected] の 6 人 のカードを保持したアドレス帳を作成している. 次に,テストスクリプトの一部を取り出 すと以下のようになる.

let

address_book = MakeAddressBook (),

new_card = mk_CARD ("new_name", "[email protected]"),

expected_book = address_book munion {new_card.Name |-> new_card}

in

post_新規カード登録 (address_book, new_card, expected_book) = true;

address bookは, 前述の MakeAddressBook 関数により作成されたテスト対象とするア

ドレス帳の値を保持し, new card は, 新規に登録するカードの値を保持している. ex-pected book は, 写像の munion (併合) 演算子を用いて, テスト実行前の address book

に new card を登録した値を保持している. let 式中で作成した変数を用いて, 「 post

新規カード登録」関数のテストを in 式中で実施している. このように, 図4.3に示した 宣言的な記述を評価するためには, 新規カード登録後のアドレス帳のテストデータ

(ex-pected book) が必要である. このデータを作るために, 「新規カード登録」関数で実施

すべきことと同様の処理をテストスクリプト側で実施している. つまり,あらかじめ登録 後のアドレス帳を作成しておかなければ, 宣言的な記述である事後条件を評価すること ができない. このため, 宣言的な記述は, 評価者の作業工数が課題となることが多い. 内 部状態の構造として, BOOK型は簡単な例であったが, 内部状態が複雑な仕様において 特に課題となることが多い.

次に, 既に示した「新規カード登録」関数と図4.7に関する,テストスクリプトの記述 から, この課題が解決できることを示す.

テストスクリプトの一部を取り出すと以下のようになる.

let

address_book = MakeAddressBook (),

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