*.exe形式のファイルをWindowsで実行するか、StuffItで解凍するとディレクトリーが生成されます。
*.zip形式のファイルは、zipを解凍できるソフトウェアを使って解凍してください。
ほかにも例題は持っているので、興味ある方はss@shinsahara.comまでメールしてください。
教科書の例題 --ジョン・フィッツジェラルド，ピーター・ゴーム・ラーセン著: 荒木 啓二郎，張 漢明，荻野 隆彦，佐原 伸，染谷 誠 訳､ソフトウェア開発のモデル化技法, 岩波書店, 2003, ISBN4-00-005609-3 C3004 のVDM-SLの例題をVDM++の例題に修正したもの
銀行 --IFAD社の例題を日本語化したもの
図書館貸出管理 --ソフトウェア工学の有名な例題である図書館貸出の分析モデル
フィッツジェラルド博士の図書館貸出管理 --上と同じ図書館貸出の分析モデルの、フィッツジェラルド博士による解
分析パターン --分析パターンをVDM++で記述した例（構築中）
非決定文を使ったバブルソートの例 -- 非決定的な構文を使った、バブルソートの例題
階乗計算の並行処理版 -- 階乗計算を再帰的かつ並行threadで処理した例
並行処理バッファーの例 -- Permission Guardを使ったバッファーを使って、供給者threadと消費者threadが並行実行する例
WaitNotifyパターンを使った排他制御の例 -- WaitNotifyパターンを使って、並行実行を意識しないバッファーを使って、供給者threadと消費者threadが排他制御して動く例
ダイエットの仕様 -- ダイエット計算に必要な機能の仕様と、回帰テストの使い方の例題です。
銀行 --IFAD社の例題を日本語化したもの