オランダ花市場
2012/11/15 形式手法の導入 © 2012, Sako Hiroshi 34
このプロジェクトを受託した
Altran Praxsis
という会社は、顧客との契約も形 式仕様の項目ベースで行い、問題が生じたときにそれがどちらの責任か が逐一明確になるようになっているiFacts: テストケースの記述
自然言語 + 形式記述
Test Design
厳密な仕様策定手順の一例
•
要求記述の内容のうち、問題領域自身の性質（システムが変える ことのできない部分）と、構築対象（システムが影響を及ぼす部分）への記述を区別する （
à
領域資産化）•
要求記述を読み、用語を切り出す•
クラスもしくは型と、関数もしくは操作の候補を見つける•
クラスの構造（型、属性、関連）に関する概略を書く•
関数／操作に関する概略を書く（シグニチャを決める）•
要求記述から不変な性質を抽出して定義する•
事前条件、事後条件もしくは定義本体を記入することによって、関 数／操作定義を完成させる、必要ならば型定義を変更する•
作成された仕様のモデルが利用者の期待や、要求中に現れる項 目や制約を満たしているかどうかをアニメーション等を通して検証 する•
以上のステップを必要なだけ繰り返す2012/11/15 形式手法の導入 © 2012, Sako Hiroshi 36
「問題領域」の語彙の充実
厳密さ ((機械処理、テスト可能))
貸出機能
:
図書館型 * 書籍型 * 利用者型-‐>
図書館型貸出機能
(lib, book, user) ==
is not yet specified pre
book in set dom lib.
登録書籍-‐-‐
書籍が登録書籍であること
and user in set lib.
登録利用者-‐-‐
利用者が登録利用者であること
and
書籍貸出可能数(lib, book) > 0
-‐-‐
書籍に貸し出し用の余裕があること
and (user in set dom lib.
貸出中and (card lib.
貸出中
(user) < 3))
-‐-‐
利用者の利用制限冊数を超えていないこと
post
-‐-‐
指定された書籍が「貸出中」に登録されている
(user in set dom RESULT.
貸出中) and (book in set
厳密さ＋読み易さ
貸出機能
:
図書館型 * 書籍型 * 利用者型-‐>
図書館型貸出機能
(lib, book, user) ==
is not yet specified pre
登録済み書籍
(lib, book)
and
登録済み利用者(lib, user)
and
貸出可能書籍(lib, book)
and
利用者貸出制限数内(lib, user)
post
書籍貸出中
(RESULT, book, user);
問題領域の語彙を充実させることに よって仕様の見通しが良くなる。
一部は仕様部品資産として残る
既存資産の進化例
Level 0
現状Level 1
現状記述Level 2
現状改善Level 3
次世代準備（既存の仕様書） 階層構造を持つ 機種共通部分と独自部分
に分かれる
（仕様の回帰テストにより）既存の日本語仕様書との一致を保証済み 全体像を把握しやすい
仕様の十分な抽象化
検索性の向上 ある関心に特化した 閲覧性がある
日本語仕様書 Ver. A
日本語仕様書 Ver. A
日本語仕様書 Ver. B 形式仕様書
Ver. X
形式仕様書 Ver. Y
日本語仕様書 Ver. C 形式仕様書
Ver. Z
日本語仕様書との対応が明確 で読みやすい記述
リファクタリング フィードバック
2012/11/15 形式手法の導入 © 2012, Sako Hiroshi 38
階層記述の例
記述階層名 記述目的 記述例
検証シナリオ階層 仕様アニメーションを行うための 検証シナリオ（テストケースなど）を 定義した階層
(
例えば非接触IC
カードの場合)
個別コマンド検証シナリオなど機能仕様階層 特定の応用に対する機能仕様を 定義する階層
カード操作コマンド仕様など 問題領域データ階層 問題領域に特有の共通データ等
を定義した階層
具体的なファイル構造など
問題領域階層 共通問題領域で繰り返し利用さ れる関数や不変条件などを定義す る階層
カードファイルシステム、データパケッ トの変換など
共通領域階層 特定の問題領域に依存しない階 層。ネットワーク（数学的な意味で）
や、組合せアルゴリズム、文字列 や数値に関する共通処理などがこ こで記述される
階層型データ処理など
学習リソース
2012/11/15 形式手法の導入 © 2012, Sako Hiroshi 40
利用できる様々なリソース
•
様々な実践ノ ウハウの提供•
実践ノウハウ の共有• VDM, B, SPIN, etc …
•
基本的な情報書籍 ツール
コンサ ルタン
ト コミュニ
ティ