電気ポットの「企画要求仕様」（リスト1）を題材にします。以下の5項目の要求が書かれています。
リスト1 企画要求仕様
PR01: 電気ポットの容量は2リットルとし、10度Cから沸騰するまでの時間は、15分以内とする。
PR02: 電源コンセントをつなぐと、直ちに作動し、ヒータで加熱を始め、沸騰に達したら、90度Cに保温する。
PR03: 再沸騰ボタンが押されたら、再沸騰を始める。
PR04: 水が加えられ、温度が低下したら、再沸騰を始める。
PR05: 保温中であれば、お湯を注ぐことができる。
分析者は、まず、企画要求の一覧（図1）を作り、要求を機能要件と非機能要件に分類しました。
図1 企画要求の一覧
続いて、分析者は、要求から状態、クラス、型、操作を抽出する作業を行いました。この作業を「要求分析」（図2）と称します。
図2 要求分析
続いて、分析者はデータフロー図（図3）を作成しました。ここまでの作業はMicrosoft Excelを使用しました。
図3 データフロー図
最後に、VDM++形式（リスト2）で仕様を記述しました。ツールはOvertureを使用しました。
リスト2 VDM++
------------------------------------------
class 「システム」
instance variables public i水温監視 : 「水温監視」;
public i水温制御 : 「水温制御」;
public i給湯制御 : 「給湯制御」;
operations
public 「システム」 : () ==> 「システム」 --初期化
「システム」() ==
(
i水温監視 := new 「水温監視」();
i水温制御 := new 「水温制御」(i水温監視);
i給湯制御 := new 「給湯制御」(i水温制御);
start(i水温監視);
start(i水温制御);
);
public 再沸騰させる : () ==> ()
再沸騰させる() ==
i水温制御.再沸騰させる();
public お湯を注ぐ : () ==> ()
お湯を注ぐ() ==
i給湯制御.給湯する();
end 「システム」
-------------------------------------------
-------------------------------------------
class 「水温監視」
types
public 「水温」 = <低温> | <高温> | <沸点> | <異状>; --高温=90℃「前後」
instance variables
public i水温 : 「水温」 := <低温>;
operations
protected 水温を監視する : () ==> ()
水温を監視する() ==
is not yet specified
post
i水温 = 水温センサの値を得る();
pure protected 水温センサの値を得る : () ==> 「水温」
水温センサの値を得る() ==
is not yet specified;
thread
while true do
水温を監視する();
end 「水温監視」
-------------------------------------------
-------------------------------------------
class 「水温制御」
types
public 「動作モード」 = <停止中> | <沸騰中> | <保温中>;
instance variables
public i動作モード : 「動作モード」;
protected i水温監視 : 「水温監視」;
operations
public 「水温制御」 : 「水温監視」 ==> 「水温制御」
「水温制御」(a水温監視) ==
(
i水温監視 := a水温監視;
);
public 再沸騰させる : () ==> ()
再沸騰させる() ==
is not yet specified
post
i動作モード = <沸騰中>;
pure protected 動作モードを決定する : () ==> 「動作モード」
動作モードを決定する() ==
is not yet specified
post
cases mk_(i水温監視.i水温, RESULT):
mk_(<沸点>,<保温中>) -> true,
mk_(<沸点>,<沸騰中>) -> false,
mk_(<高温>,<保温中>) -> true,
mk_(<高温>,<沸騰中>) -> true,
mk_(<低温>,<保温中>) -> false,
mk_(<低温>,<沸騰中>) -> true,
mk_(<異状>,<停止中>) -> true,
others -> false
end
and i動作モード = RESULT;
protected ヒータを制御する : () ==> ()
ヒータを制御する() ==
is not yet specified
post
i動作モード = 動作モードを決定する();
thread
while true do
ヒータを制御する();
end 「水温制御」
-------------------------------------------
-------------------------------------------
class 「給湯制御」
instance variables
protected i水温制御 : 「水温制御」;
operations
public 「給湯制御」 : 「水温制御」 ==> 「給湯制御」
「給湯制御」(a水温制御) ==
(
i水温制御 := a水温制御;
);
public 給湯する : () ==> ()
給湯する() ==
is not yet specified
pre
i水温制御.i動作モード = <保温中>;
end 「給湯制御」
-------------------------------------------
参考までに、別の分析者がVDM-SLで記述したものをリスト3に示します。このVDM-SLの記述はOvertureにインポートして見ることができます。
リスト3 VDM-SL
/*
* PR01 : 電気ポットの容量は 2 リットルとし、10 度 C から沸騰するまでの時間は、15 分以内とする。
*
* PR02 : 電源コンセントをつなぐと、直ちに作動し、ヒータで加熱を始め、沸騰に達したら、90 度 C に保温する。
*
* PR03 : 再沸騰ボタンが押されたら、再沸騰を始める。
*
* PR04 : 水が加えられ、温度が低下したら、再沸騰を始める。
*
* PR05 : 保温中であれば、お湯を注ぐことができる。
*/
types
水量型 = int /* 単位はミリリットルとする。 */
inv 水量 == 0 <= 水量 and 水量 <= 2000; /* PR01 */
水温型 = int /* 単位は摂氏とする。 */
inv 水温 == 0 <= 水温 and 水温 <= 100;
ポットの状態型 = <電力が供給されていない> | <沸騰するまで加熱せよ> | <保温せよ>;
ヒーターの状態型 = <停止> | <加熱> | <自動>
/* 「自動」とは、保温のために自動的にONとOFFを切り替えることである。 */
values
state ポット of
ポットの状態: ポットの状態型
ヒーターの状態: ヒーターの状態型
水量: 水量型
水温: 水温型
init
状態 == 状態.ポットの状態 = <電力が供給されていない>
and 状態.ヒーターの状態 = <停止>>
and 0 < 状態.水量 and 状態.水量 <= 2000
and 0 <= 状態.水温 and 状態.水温 < 100
inv
状態 == true
end
