VDM++

VDM++(Vienna Development Method++)

オブジェクト指向、アーキテクチャ/部品

VDM-SLをオブジェクト指向拡張したもの

事例

Felica Networksで使用されたらしい

Suicaのシステムは要件定義部分でVDM++が使用された

VMD++の例

code:memo

class イベント参加登録管理システム

登録済みユーザ集合 : set of 「ユーザ識別子」;

定員 : nat1;

inv card 登録済みユーザ集合 <= 定員 // システム状態の制約

抽選登録する : set of 「ユーザ識別子」 ==> 「ユーザ識別子」

抽選登録する(引数ユーザ集合) == is not yet specified

pre // 操作実行の前提となる事前条件

card 登録済みユーザ集合 < 定員 // 定員未満のときのみ受付

post

登録済みユーザ集合 = 登録済みユーザ集合~ union {RESULT}

and RESULT in set 引数ユーザ集合

and RESULT not in set 登録済みユーザ集合~;

// 事後条件：実行後には、引数の中から未登録の人が1人

//登録されていることをもって正しい操作だと判断する

開発ツール

参考