本ページの内容はあくまで著者がまとめた「簡単に触ってみる第一歩」（VDMTools 8.3.1で確認）ですので，詳細なツール仕様や最新の情報については，各ツールの公式Webサイト・マニュアル等をご確認下さい．
大きな画像は縮小しており，クリックすると大きな画像が表示されます．
取得・インストール
Webサイトからダウンロードできます．サイトに登録するとLite版が利用できるようになります．ダウンロードはVDM-SLやVDM++等扱う言語ごと，また対象OSごとに分かれています（例： VDM-SL ToolboxのWindows版）．
一般のプログラム同様にインストーラを起動しインストールします．
初期設定・画面の見方
立ち上げたらまず，メニューの「プロジェクト」→「ツールオプション」から，文字コードを日本語（Shift-JIS等）に設定して下さい．この設定をしないと，日本語が含まれたファイルが文字化けします．
Toolboxのウィンドウ内では，インタプリタ等様々なウィンドウを表示することができます．ウィンドウの表示・非表示は，メニューの「ウィンドウ」から行うか，ツールバーのボタンから行うことができます．個々のウィンドウの右上には，（Toolboxのウィンドウ内での）最小化・最大化・閉じるボタンが付いています．Toolbox内のウィンドウを誤って最大化してしまい，他のウィンドウが見えなくなってしまうことがたまにあるので注意して下さい．
プロジェクト・ファイルの管理
メニューの「プロジェクト」から，もしくはツールバーの「＋」「－」ボタンから，ファイルをToolboxに読み込ませたり，読み込みをやめたり（ファイル自体は消されません）することができます．
またメニューの「プロジェクト」から，もしくはツールバーのボタンから，このファイルを読み込んだ状態や設定などをプロジェクト（prjファイル）として保存したり，それをまた読み出したりすることができます．プロジェクトを保存すると，以後インタプリタでファイルを指定するときに該当prjファイルのあるフォルダからの相対パスで指定することもできるようになります．
仕様記述の編集
「マネージャー」ウィンドウに表示される読み込んだファイルをダブりクリックすると，「ビューア」（ソースウィンドウ）が立ち上がります．これは仕様を読むだけです．
仕様の編集は，Overture IDEなど，好きな外部エディタを用いて行います．外部エディタ上で変更し保存すると，Toolbox側で再読み込みするはずです（万が一自動で最新のものを読み込まない場合にはいったんファイルの読み込みを外して，再度読んでみて下さい．）．
読み込み時・再読み込み時には，自動で構文チェックが行われます．「マネージャー」ウィンドウで「モジュール」（VDM-SLの場合）または「クラス」（VDM++の場合）というタブを開くと，各モジュール・クラスの状態が表示されます．「S」というのは構文（syntax）チェック済みということを表します．メニューの「アクション」から，もしくはツールバーのチェックマークが付いた各種ボタンから，モジュール・クラスに対する処理を呼び出すことができます．構文チェックは自動で行われますが，それに加え必ず型チェックを行っておくとよいでしょう．
実行
メニューの「ウィンドウ」→「実行」から，もしくはツールバーの虫（バグ）がつぶされているようなボタンから，実行ウィンドウ（インタプリタ）を開くことができます．ここではインタラクティブにコマンドを実行していくことができ，上下キーを押してコマンド履歴を呼び出すこともできます．例えば，printコマンドを使って随時操作の呼び出しをしていき戻り値を見ていくことができます．ファイルに記述しておいたコマンドを一斉に実行するようなこともできます（scriptコマンド）．利用可能なコマンドは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)
デバッグ
ビューア（ソースウィンドウ）printではなくdebugコマンドを使うと，デバッグモードでの実行になります．その前にbreakコマンドを用い関数や操作を指定し，ブレイクポイントを指定することができます．ブレイクポイントで一時停止した後は，ステップ実行等を行うことができます，
以上が基本的な使い方になります．
© Fuyuki Ishikawa, National Institute of Informatics, Japan, 2011-