データ構造の隠蔽による仕様と設計の分離方法の提案

拡張陽関数定義を用いることで,仕様伝達部と非伝達部を分離して,仕様伝達部におい て入出力の関係を宣言的に記述することができるため,「解決すべき問題」であるWhat を記述することができる. したがって, この宣言的な記述箇所において, 操作的な記述を 行わなければ,「実行可能性の影響」を回避することができる.

次の4.2節では, 2 つ目の研究課題である, 仕様と設計の分離の課題を解決する形式仕 様記述の設計・構成法を提案する. その次の4.3節において, 本節において述べた, 記述 スタイルの提案手法について, 具体的な仕様記述例を用いて評価する.

4.2 データ構造の隠蔽による仕様と設計の分離方法の提案

本節では, 本章において扱う 2 つ目の課題である, 仕様と設計の分離に関する課題を 解決する形式仕様記述の設計・構成法を提案する.

2.1.2節で述べたように, 仕様と設計の分離とは, 「解決すべき問題」を定義した仕様

と, 「問題の解決方法」を定義した設計を分けて考えるということである. 一般に, 仕様 策定工程では,何を作るべきかという「解決すべき問題」を検討し,設計工程では, 「問 題の解決方法」を検討することで,仕様策定者と設計者が分業して組織的に開発を行うこ とができると言われている. 仕様と設計の分離は広く言われていることではあるが,実際 に, 仕様と設計を分離することは容易ではない. 仕様と設計の境界が曖昧であるために, 形式仕様記述から仕様として規定している範囲と,形式仕様記述には記述してはあるが, 設計者が自由に規定できる範囲を, 設計者が読み取ることが難しいという課題がある.

本研究では,仕様と設計の分離を行うために,開発対象の内部状態を表す内部データ構 造に着目した. 形式仕様記述言語には, 集合や写像などの内部データ構造を抽象化する ための型が用意されている. しかし, 集合や写像を用いて内部データ構造を表現したと しても, 型の特性から設計者に仕様と設計の責任範囲を伝えることはできない. 以下に, この課題に関する具体的な例を示す. 例えば, 名前(NAME 型)とアドレス (ADDRESS 型) からなるアドレス帳 (BOOK 型) について考える. 名前 (NAME 型) とアドレス

(ADDRESS 型) を次のように定義する.

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

NAME = seq of char;

ADDRESS = seq of char;

ここで, 名前 (NAME 型) とアドレス (ADDRESS 型) は仕様策定者が仕様として規定

している型とし, アドレス帳 (BOOK 型) の保持方法は設計者が規定すべきことと仮定 する. つまり, 仕様と設計が分離された仕様記述であるためには, 上記の, 仕様として規 定している型と, 設計者が規定すべき型の仮定が, 仕様記述から読み取れなければならな い. 実行可能仕様を記述するためには,アドレス帳(BOOK 型)の型を決める必要がある. BOOK 型を, 内部データ構造を抽象化するために用意された集合と写像の型を用いて規 定した例を示す. 写像を用いた場合を BOOK1 型とし, 集合を用いた場合を BOOK2 型 とすると,次のような記述になる.

BOOK1= map NAME to ADDRESS;

BOOK2= set of CARD;

ここで, CARD 型はレコード型である. レコード型は複数の型をまとめて管理すること

ができる. CARD型の型定義を次に示す.

CARD ::

Name : NAME

Address : ADDRESS;

この型の値は、レコード型の構成子を用いて次の表に定義する。

mk_CARD ("name", "[email protected]")

このようにして, Name に “name” という文字列を保持し, Address に “[email protected]”

という文字列を保持した CARD 型の値を定義することができる. ここでは, CARD 型 も BOOK 型と同様に,形式仕様記述には記述してあるが,設計者が自由に決めることが できる型とする.

次に, 名前とアドレスをアドレス帳(BOOK 型) へ新規に登録する仕様を考える. 前述

のBOOK1 型であってもBOOK2 型であっても,新規に名前とアドレスを登録する仕様

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

4.2. データ構造の隠蔽による仕様と設計の分離方法の提案 61

を記述することができる. 事後条件は,登録後のアドレス帳(BOOK1 型, BOOK2型)に 指定した登録対象の名前とアドレスが存在していることとした. 事前条件として,既に同

一の名前 (NAME 型) がアドレス帳に登録されていないこととした.

写像を用いて定義した BOOK1 型を用いると次のような記述になる. public 新規カード登録 1 : BOOK1 * NAME * ADDRESS -> BOOK1 新規カード登録 1 (bk, name, addr) ==

bk munion {name |-> addr}

pre name not in set dom bk

post RESULT = bk munion {name |-> addr};

次に, CARD型の集合を用いた BOOK2 型を用いた場合, 次のような記述となる.

public 新規カード登録 2 : BOOK2 * NAME * ADDRESS -> BOOK2 新規カード登録 2 (bk, name, addr) ==

bk union {mk_CARD (name, addr)}

pre forall c in set bk & c.Name <> name post mk_CARD (name, addr) in set RESULT;

ここでは, いずれの型定義であっても, 仕様が記述可能であることを示すまでにとどめ

ておいて, 詳細な VDM++ の言語仕様の説明は省略する. BOOK1 型を用いた場合も,

BOOK2 型を用いた場合も, 事前条件と事後条件において記述している内容は同じであ

る. しかし,設計者はどちらの表現であっても, NAME 型と ADDRESS 型は仕様におい て規定する型であることを読み取ることができない. 同様に, CARD 型と BOOK 型は 設計者が自由に定義することが許された型であることを読み取ることができない.

この課題を解決するために,本論文では,仕様と設計の境界部分として内部データ構造 に着目し,仕様として規定しない型を隠蔽することで, 仕様策定者が仕様として規定する 型と, 仕様策定者が仕様としては規定せずに,設計者の責任範囲として規定すべき型の違 いを明示する方法を提案する. 型を隠蔽した場合と,隠蔽しない場合を比較し,可読性の 違いを比較する.

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

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

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

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

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