チュートリアル資料
以下サイトから、チュートリアルのドキュメントと、チュートリアルで使用する演習問題がダウンロードできます。
チュートリアルの概要
- 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」を実行しました。
感想
チュートリアルを通じて、開発ツールの使い方や、言語仕様の雰囲気はつかめました。なんだかよく分かっていない部分も多いので、次は一から実装してみたいと思います。