チュートリアル資料

　以下サイトから、チュートリアルのドキュメントと、チュートリアルで使用する演習問題がダウンロードできます。

形式手法入門 VDM++チュートリアル（IPA）

チュートリアルの概要

VDMツールのインストールと設定（Overture Tools、VDMTools）
VDM++言語入門（例題を通じた説明等）

読み替えを行った箇所など

　チュートリアルの資料が2016年時点のものであるため、現状の最新バージョンに即していない記載や、やや分かりにくい記載がありました。以下に補足します。ちなみに私が実行したのは、Windows版です。

p10：インストーラは、VDL Toolsの「VDM-SL」ではなく「VDM++」をダウンロードしました。
p18 : セットアップ直後は、プロジェクトがまだないので本ページの設定（プロジェクト設定）ができませんでした。そのため本手順は、チュートリアルプロジェクトの読み込み後に実施しました。
p23 : workspaceに指定するフォルダは、「\seminar_tokyo_20160229-02\Fare0」としました（その下にもFare0フォルダがありますが、それを指定するとうまくいきませんでした）
p26 : 具体的な操作手順が記載されていなかったので補足します。「Fare0_testspec.vdmpp」を右クリックして、「Debug Configurations..」を実行しました。Nameには任意の名前を入力し、ProjectはFare0を指定、Entry Pointは「Serach」ボタンから「Test()のrun()」を指定しました。
p28 :具体的な操作手順が記載されていなかったので補足します。メニューバー「実行⇒初期化」を行うと、実行ウインドウが表示されます。実行ウインドウ株の「>>」に、資料記載のコマンド（traces UseFare0）を入力し、エンターを押します。
p29 : 資料上では「Window -> Open Perspective」となっていますが、存在しませんでした。そのため、「Window ->　Perspective -> Open Perspective」と操作しました。また、画面右部（CT Overviewタブ）のT0、T1はそれぞれ右クリックし「Full Evaluation」を実行しました。

感想

　チュートリアルを通じて、開発ツールの使い方や、言語仕様の雰囲気はつかめました。なんだかよく分かっていない部分も多いので、次は一から実装してみたいと思います。

（参考）使用したインストーラ