形式記述言語VDM++の制御構文（例外処理）をJava C# Re:Mind(自作言語)と比較

# はじめに

要求仕様記述段階での使用が主に想定されている数学的形式手法VDM(Vienna Development Method)[^1]のオブジェクト指向拡張言語VDM++ですが、ロジックの実装も記述できる構文が用意されています。本記事ではVDM++の制御構文（例外処理）をJavaとC#そして自作言語のRe:Mind[^2] と比較してみます。

## この記事内容の作業目的
VDM++の下記の制御構文[^3][^4]についていくつかの記事に分割して比較検討します。クラスの定義構文についてはこちらの記事[^5]を参照することができます。

・ブロック文
・コメント文
・代入文
・条件文
・ループ文
・call文
・return文
・**例外処理**　←本記事対象

VDM++はオブジェクト指向言語的な言語要素を持ち、数学的形式手法言語の中では一般のプログラミング言語のオブジェクト指向言語に近い面があります。

Re:MindはJavaやC#の経験者向けに設計された日本語プログラミング言語の一種で、ロジック仕様記述言語とトランスコンパイラ言語とで言語仕様を共有しています。

ロジック仕様記述言語は疑似言語みたいなものですから、コンパイラを通さないことを前提にするならば未定義の関数を要件表記として使うこともできます。自然言語の日本語で記述するよりは厳密な構造的な記述が可能です。

VDMのような数学的形式手法を使わない場合は、一般的に自然言語の日本語で要求仕様が記述されているものと推察されます。本記事では数学的形式手法と自然言語の日本語記述とのはざまで、構造化された日本語が要求仕様記述に使えないか模索しています。

## この記事内容の保証
各言語で書かれた引用ソースの妥当性は保証されません。また、本記事に開示された自作言語の仕様は、開発中の仕様のため予告なく変更される場合があります。

# 構文比較
## VDM++
```vdm:VDM++
    doAnything: () ==> ()
    doAnything() ==
    (
        trap p with ExceptionOccured(p) in
        ( 
            always finallyTodo in
            ( 
              -- todo 例外がスローされる余地のある処理
            )
        )
    );
```
VDM++の例外処理はalways s1 in s2のs2で例外が生じる範囲を指定し、その範囲をさらにtrap p with s1 in s2のs2で囲うことでalwaysの範囲で生じた例外をトラップする。
always s1のs1は例外がスローされてもされなくても通過する処理
trap p with s1のs1は例外がスローされた場合に通過する処理で、パターンpとの合致が評価されて、合致しない場合は実行されない。

```vdm:VDM++
    doAnything: () ==> ()
    doAnything() ==
    (
        trap p with ExceptionOccured(p) in
        ( 
            always todo1 in
            ( 
              -- todo2 例外がスローされる余地のある処理
              -- exit 文を用いて例外が発生したことを通知できる
              -- 式e はどのような種類の例外が起きたのかを知らせる。
              exit e
            )
        )
    );
```
exit 文を用いて例外が発生したことを通知できる。
式e はどのような種類の例外が起きたのかを知らせる。
## Java
```java:Java
    try{
        //todo 例外がスローされる余地のある処理
    }catch(Exception e){
        //例外の処理 例外型はサンプル
    }
```
Javaは例外処理try～catch文をサポートします。

```java:Java
    try{
        //todo 例外がスローされる余地のある処理
    }catch(Exception e){
        //例外の処理 この例外型はサンプル　例外型変数の持つ関数が使える
        throw new Exception("エラーの意味がわかるメッセージ");
    }finally{
        //finallyTodo例外がスローされてもされなくても通過する処理
        //"エラーの意味がわかるメッセージ"例外がスローされた後も通過します。
    }
```
throw文で新しい例外を投げることができます。
例外がスローされてもされなくても通過する処理finally句もオプショナルに記述できます。
```java:Java
    try{
        //todo 例外がスローされる余地のある処理
    }catch(Exception e){
        //例外の処理 この例外型はサンプル　例外型変数の持つ関数が使える
    }catch(Exception2 e){
        //別の例外型の処理 この例外型はサンプル　例外型変数の持つ関数が使える
    }finally{
        //例外がスローされてもされなくても通過する処理
    }
```
catch文で補足する例外型を指定して、特定例外だけの処理を記述することができます。

## C#
```cs:C#
    try{
        //todo 例外がスローされる余地のある処理
    }catch(Exception e){
        //例外の処理 この例外型はサンプル　例外型変数の持つ関数が使える
    }
```

C#は例外処理try～catch文をサポートします。


```cs:C#
    try{
        //todo 例外がスローされる余地のある処理
    }catch(Exception e){
        //例外の処理 この例外型はサンプル　例外型変数の持つ関数が使える
        throw new Exception("エラーの意味がわかるメッセージ");
    }finally{
        //finallyTodo例外がスローされてもされなくても通過する処理
        //"エラーの意味がわかるメッセージ"例外がスローされた後も通過します。
    }
```
throw文で新しい例外を投げることができます。
例外がスローされてもされなくても通過する処理finally句もオプショナルに記述できます。

```cs:C#
    try{
        //todo 例外がスローされる余地のある処理
    }catch(Exception e){
        //例外の処理 この例外型はサンプル　例外型変数の持つ関数が使える
    }catch(Exception2 e){
        //別の例外型の処理 この例外型はサンプル　例外型変数の持つ関数が使える
    }finally{
        //例外がスローされてもされなくても通過する処理
    }
```
catch文で補足する例外型を指定して、特定例外だけの処理を記述することができます。

## Re:Mind
```mind:Re:Mind
    ◇試す
        //todo 例外がスローされる余地のある処理
    ◇捉まえる(Exception e)
        //例外の処理 この例外型はサンプル　例外型変数の持つ関数が使える
    ◇ここまで
```
Re:Mindはターゲット言語が例外処理try～catch文をサポートする場合はサポートします。◇の直後の「試す」と「捉まえる」は予約語となります。

```mind:Re:Mind
    ◇試す
        //todo 例外がスローされる余地のある処理
    ◇捉まえる(Exception e)
        //例外の処理 この例外型はサンプル　例外型変数の持つ関数が使える
        投げる new Exception("エラーの意味がわかるメッセージ");
    ◇必ず最後に
        //finallyTodo例外がスローされてもされなくても通過する処理
        //"エラーの意味がわかるメッセージ"例外がスローされた後も通過します。
    ◇ここまで
```
「投げる」文で新しい例外を投げることができます。
new Exceptionはターゲット言語の構文をそのまま使います。
例外がスローされてもされなくても通過する処理「必ず最後に」句もオプショナルに記述できます。
◇の直後の「必ず最後に」は予約語となります。

```mind:Re:Mind
    ◇試す
        //todo 例外がスローされる余地のある処理
    ◇捉まえる(Exception e)
        //例外の処理 例外型はサンプル
    ◇捉まえる(Exception2 e)
        //別の例外の処理 例外型はサンプル
    ◇必ず最後に
        //例外がスローされてもされなくても通過する処理
    ◇ここまで
```

「捉まえる」文で補足する例外型を指定して、特定例外だけの処理を記述することができます。

# おわりに
VDM++はC/C++やJavaに近くプログラマに馴染みやすいとされていますが、いかがでしたでしょうか？VDM++は例外のキャッチ範囲をブロック文の入れ子で構成しているようです。alwaysのブロック文で例外の発生範囲を指定して、trapのブロック文でさらにその範囲を囲む感じ。
trapのブロック文がないalwaysのブロック文はJavaやC#でいうcatch句のブロック文になにも書かないことに対応するような気がしました。
また、trapのパターンpにより、with句の関数に引数として渡して実行するしないが制御されるのはcatch句で型を指定して処理する句を選択できるのに似ているのかもしれません。


[^1]: IBMのウィーン研究所で1960年代から70年代にかけて開発された形式手法。その実装には1996年にISO標準（ISO_IEC_13817-1）となったVDM-SLと、そのオブジェクト指向拡張のVDM++がある。
[^2]: Qiita [オープンな設計言語仕様 日本語ロジック仕様記述言語 Re:Mind（リマインド）](https://qiita.com/mylifewithviolin/items/52f806777e6ea031de94) 参照
[^3]: FMVDM　[VDMTools 付属文書](http://fmvdm.org/doc/index-ja.h
[^4]: FMVDM-> github [[PDF] VDMTools VDM 言語マニュアル VDM++](https://github.com/vdmtools/vdmtools/raw/stable/doc-jp/lang-man/langmanpp_a4J.pdf)
[^5]: Qiita [要求仕様 形式記述言語VDM++ との構文比較 ロジック仕様記述言語 Re:Mind（リマインド）](https://qiita.com/mylifewithviolin/items/2a8c6dc66cead04536a8)