# vdmの実行方法について

### 実行環境の取得
1. フォルダを作成

2. 1のフォルダにvdmjのファイルをダウンロード
https://github.com/nickbattle/vdmj に移動
右の真ん中の方の「4.4.6Release」(数字は、その時のバージョンによる)をクリック
Assetsの中の「java・・.jar」ファイルをクリックしてダウンロード
ファイルをフォルダに移動

3. 練習用のファイルを1のフォルダに作成する
vscodeで1のフォルダを開く
ファイルを作成する。名前を「practice.vdmpp」に変更する
以下を作成したファイルにコピペ

class practice    -- classを作成します

types    -- 型を設定します。（C言語の構造体のイメージ）
    
    public book::                           -- public 変数名:: でbookという構造体を設定する この中に構造体に含まれる型を設定する
        book_number : int                   -- 本の番号を示す
        borrowing_or_not : bool             -- 本が借りられているかどうかを表現する bool型で表される
        book_name : token;                   -- 本の名前を示す。  token型はvdmの文字列型
            

instance variables                                                 -- 大域変数を設定します。
    public library_books : book := mk_book(1, false, mk_token("book_A"));                      -- 図書館の本を示す。 book型はtypesで作成した型である。 自分で作成した型を用いるときはそれぞれの要素の場所で「mk_要素の型()」と記述する　 
                        

operations                              -- 操作を示す
    public borrow_book:  int ==> ()         -- 操作の名前、引数の型、返却値の型を示す
        borrow_book(book_number) == (       -- 操作の名前、引数の名前を示す
            library_books.borrowing_or_not := true;  --本を借りている状態にする
        )
        pre book_number = library_books.book_number;  -- 事前条件として図書館の本の番号と引数の番号が同じ

    public return_book:  () ==> ()
        return_book() == (
            library_books.borrowing_or_not := false;
        );


functions

end practice

#### 上のプログラムの概要
- 本の貸し借りに関するvdm
- borrow_bookを実行することで、本を借りる動作を行う（本の借りられているかどうかの変数を借りられているに変更する）
- return_bookを行うことで本を返す動作を行う
- borrow_bookには引数として本の番号（int型）があり、事前条件として引数の本の番号と、大域変数の本の番号が同じである必要がある。

4. vscodeでターミナルを開き、以下を入力

java -jar vdmj-3.1.1-160630.jar -vdmpp -i practice.vdmpp

⚠️　青色の場所の数字は自分のダウンロードしたファイルのバージョン（ファイル名）に変更してください

5. 以下の画面が出るとOK

- 以下のエラーが出た場合は、javaのバージョンを落としてください
Exception in thread “main” java.lang.IncompatibleClassChangeError: class com.fujitsu.vdmj.scheduler.SchedulableThread overrides final method java.lang.Thread.isVirtual()Z
at java.base/java.lang.ClassLoader.defineClass1(Native Method)

---

### 実行する(上記の5の続きから行う)

> の部分に以下を入力する（入力した後にenter）
6. インスタンスを作成する
create test := new practice()

7. print インスタンス.大域変数で大域変数の値を確認する
print test.library_books

8. 本の借りる動作を行う
print test.borrow_book(1)

9. 値が変更されたのを確認
print test.library_books

10. 本を返す動作を行う
print test.return_book()

11. 値が変更されたのを確認
print test

12. 事前条件に違反することを確かめる
print test.borrow_book(3)

13. 事前条件に違反する前の画面に戻る
quit

14. 値が変わっていないことを確認
print test

15. 終了する
quit