本ページの内容はあくまで著者がまとめた「簡単に触ってみる第一歩」（Overture IDE 1.1.0 RC1で確認）ですので，詳細なツール仕様や最新の情報については，各ツールの公式Webサイト・マニュアル等をご確認下さい．
大きな画像は縮小しており，クリックすると大きな画像が表示されます．
取得・インストール
sourceforgeからダウンロードできます．目立つところにあるリンクはWindows 32bit版ですが，Filesというリンクから他のバージョン（64bitやMac，Linux版）や，新しいバージョンのRC版等をダウンロードできます．VDM-SL，VDM++いずれを用いる場合でもツールは同じです．
適当なところに解凍して設置します．中にある overture という実行ファイル（Windowsであれば overture.exe ）を実行すると立ち上がります．必要に応じてスタートメニュー等への登録を行って下さい．
初期設定・画面の見方
立ち上げると Workspace の設定ダイアログが出ます．ここでは諸々の作業ファイルを保存するフォルダを指定して下さい．その後初期ウィンドウが出ますが，表示されている情報が特に必要なければこのウィンドウ（Overture IDE画面内でのウィンドウ）を消して下さい．
通常のEclipseと同様，画面内に多くのウィンドウが表示され，個々をドラッグで移動したり表示しないよう「×」ボタンを押して削除したりすることができます．特定の作業に有用なウィンドウの集まりを「パースペクティブ」と呼びます．例えば，VDMを編集するためのVDMパースペクティブ，デバッグを行うためのDebugパースペクティブ等があります．現在のパースペクティブは右上に表示されており，そこからパースペクティブを切り替えることができます．パースペクティブの切り替えやウィンドウの表示は，メニューのWindowからも行うことができます．
プロジェクト・ファイルの作成
メニューのFileから，もしくは左にあるVDM Explorerウィンドウのコンテキストメニュー（右クリック）から，Newを選びプロジェクトを作成します．VDM-SLプロジェクトまたはVDM-PP（VDM++）プロジェクトのいずれかを選び，プロジェクト名を入力します．ここでFinishを押さずにNextを押すと，インポートする標準ライブラリを選ぶことができます．単にファイルがコピーされるだけ（特に「パスを通す」ような設定があるわけではない）なので，とりあえず全部インポートしておいていらないものを消してもよいでしょう．
左にあるVDM Explorerウィンドウのコンテキストメニュー（右クリック）から，Newを選びVDM-SLではmoduleを，VDM++ではclassを選び，名前を付けて新しい記述ファイルを作成できます．
もし既存の記述ファイルを使う場合，ファイルシステム上でコピーしてworkspaceフォルダ内に貼り付け，VDM Explorer上でコンテキストメニューからRefleshします．このとき，VDM Explorer上に直接貼り付けることもできます．
仕様記述の編集
エディタ上でどんどん入力をしていきます．文法等のチェックはオンラインで（記入中に随時）行われ，エラーがある部分は赤くなります．赤く「×」が付いている部分にカーソルを当てるとエラー内容がわかります．エラー内容は下部にあるError Logウィンドウにも表示されます．
変数名等の自動補完は，Alt+/で行うことができます．
特定のキーワード（の一部）を打ち込んでCtrl+Spaceを押すとテンプレートを挿入することができます．例えば op と打った後だと，操作定義（操作定義開始宣言，陰定義，陽定義それぞれ）のテンプレートを選んで挿入することができます．テンプレート挿入後にはTabを押して次の入力項目に移動できます．利用可能なテンプレートは，メニューのWindow→Preferences→VDM→Templatesから確認できます．（下図はVDM++での陽操作定義のテンプレート）
実行
計算式の結果確認
個々の式を実行してみて結果を確認したい場合，Quick Interpreterを用います．ここでは記述ファイルに関係なく，1つ1つの式の実行結果を確認することのみできます．
関数・操作を指定しての実行
仕様記述の実行・テストをする場合，メニューのRunから（もしくはツールバーの再生ボタンのようなものから）Run Configurationを選びます．Launch Modeが最初Entry Pointになっていますが，これは特定のメソッドを実行するものです．多くの場合，作成したテスト操作を呼ぶ際に用いるかと思います．Searchボタンを押すと，読み込まれているモジュール・クラスの関数・操作が表示されるので，そこから呼び出したいものを選びます（Module/Class，Function/Operationの欄をテキストで直接書いてもかまいません）．必要であれば，Function/Operationの関数・操作のところに記入されている仮引数を，具体的な値に変更します．
インタラクティブコンソールでの実行
先の画面のLaunch ModeをConsoleにすると，インタラクティブにコマンドを実行していくことができます．例えば，printコマンドを使って随時操作の呼び出しをしていき戻り値を見ていくことができます．利用可能なコマンドはhelpコマンドで表示させることができます．
printコマンドを用いる場合，printに続けてVDM-SL/VDM++の式（代入文の右辺などに用いるような，値を導くもの）を記述します．
VDM-SLの場合，例えば以下のようにモジュール内の操作を呼んでその結果を表示させることができます（「このモジュールの（変数，操作等）」ということを表す際にはバッククオートでつなぎます）．
print module_name`operation_name(arg1, arg2)
VDM++において，静的（static）メソッドを呼ぶ場合は同様な（バッククオートを用いた）記述になります．
print class_name`operation_name(arg1, arg2)
VDM++においてインスタンスメソッドを呼びたい場合は下記のようなコマンドになります（インスタンス要素の場合には，バッククオートではなくピリオドを使います）．
print new class_name().operation_name(arg1, arg2)
上のコマンドでは「インスタンスを作成して，次にメソッドを呼ぶ」ということをして，その結果を表示しています．下記のように2コマンドに分けることもできます（この場合はインタプリタがtという名前でインスタンスを記憶しています）．
create t := new class_name() print t.operation_name(arg1, arg2)
デバッグ
RunではなくDebugとして起動した場合，もしくは実行中に実行エラーや事前条件違反等が起きた場合，Debugパースペクティブが表示され，その時点での変数の値を見たりステップ実行を試みたりすることができます．このあたりは通常のプログラミング言語向けのEclipseの利用と同様です．
VDMToolsとの併用
メニューのWindow→Preferences→VDMからVDMToolsの各実行ファイルパスを設定しておくと，VDM Explorer上のプロジェクト名のコンテキストメニュー（右クリック）で，そのプロジェクトをVDMToolsで開くことができます．例えば，仕様の編集はOverture IDEで行い，他の機能はVDMToolsを利用する，といった使い方ができます．
以上が基本的な使い方になります．
© Fuyuki Ishikawa, National Institute of Informatics, Japan, 2011-