本ページの内容はあくまで著者がまとめた「簡単に触ってみる第一歩」(Overture IDE 1.1.0 RC1,VDMTools 8.3.1で確認)ですので,詳細なツール仕様や最新の情報については,各ツールの公式Webサイト・マニュアル等をご確認下さい.
大きな画像は縮小しており,クリックすると大きな画像が表示されます.
UMLリンク
VDM++とUMLクラス図の間の相互変換を行う機能です.XMIファイル入出力に対応したastah*などのUMLツールと連携させることができます.本ページ執筆の時点ではVDMToolsにおける動作確認のみしており,そちらの情報だけ載せています.
UMLリンクの使い方(VDMToolsの場合)
基本的な使い方
VDM++ Toolboxにてメニューから「ウィンドウ」→「UMLリンク」として,もしくはツールバーからバラ(?)のアイコンを押して,機能を起動することができます.このとき,
- VDM++記述が読み込まれていない場合,クラス図からVDM++記述を生成するのであろうとして,読み取るXMIファイルを指定するダイアログが表示されます.
- VDM++記述が読み込まれている場合,このときプロジェクトを保存していない場合は,プロジェクトファイルの保存先を指定するダイアログが出ます.
いずれにしてもUMLリンクウィンドウが表示されます.この画面では,VDM++記述とUMLクラス図との差分を表示させたり,片方からもう片方を生成したりすることができます.
留意事項
一般的なUMLツールは,C++やJavaにおけるオブジェクト指向の概念や型などの語彙を認識しますが,VDM++固有の概念や語彙は認識しません.このため,例えば下記のような留意事項があります.
- クラス図上での関数と操作の区別には,ステレオタイプを用いる.
- クラス図上での事前・事後条件の記述は,precondition・postconditionというタグに対して関連づけられた値として行う.不変条件は扱われない.
- VDM++からクラス図への変換時に,setやnatといった型はクラスとして定義される(型が未定義という指摘を避けるため便宜上そうしていると思われる).
- VDM++ではパッケージの概念はないので,パッケージのないクラス図のみを対象とする.
VDM++からクラス図への変換時には,クラスが保持している写像変数の情報などから,関連や多重度などの情報がクラス図に埋め込まれます.こういった振る舞いについては,ぜひご自身でいろいろな記述に対する変換を試してみて下さい.
© Fuyuki Ishikawa, National Institute of Informatics, Japan, 2011-