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

# はじめに

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

## この記事内容の作業目的
VDM++の下記の制御構文[^3][^4]についていくつかの記事に分割して比較検討します。

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

VDM++はオブジェクト指向言語的な言語要素を持ち、数学的形式手法言語の中では一般のプログラミング言語のオブジェクト指向言語に近い面があります。また、VDMのような数学的形式手法を使わない場合は、一般的に自然言語の日本語で要求仕様が記述されているものと推察されます。本記事では数学的形式手法と自然言語の日本語記述とのはざまで、構造化された日本語が要求仕様記述に使えないか模索しています。

クラスの定義構文についてはこちらの記事[^5]を参照することができます。

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

# 構文比較
## VDM++
```vdm:VDM++
    i:int := 0,
    while i<10 do
    (
        --todo
        i := i + 1;
    );
    
```
VDM++は前判定繰り返し構文while文をサポートします。

## Java
```java:Java
    int i=0;
    while (i<10) {
        //todo
        i++;
    }
```
Javaは前判定繰り返し構文while文をサポートします。
```java:Java
    int i=0;
    do {
        //todo
        i++;
    } while (i<10);
```
Javaは後判定繰り返し構文do-while文をサポートします。
```java:Java
    int i=0;
    int j=0;
    int k=0;
    while (i<10) {
        //todo
        k++;
        j++;
        if(j>8) break;
        if(k<4) continue;
        i++;
    }
```
ループ本体内に条件分岐式を記述して、while文の判定が成立する前にループを脱出したり(break)、ループの先頭に復帰(continue)してループ本体の処理をスキップさせることができます。
## C#
```cs:C#
    int i=0;
    while (i<10) {
        //todo
        i++;
    }
```
```cs:C#
    int i=0;
    do {
        //todo
        i++;
    } while (i<10);
```
C#は後判定繰り返し構文do-while文をサポートします。
```cs:C#
    int i=0;
    int j=0;
    int k=0;
    while (i<10) {
        //todo
        k++;
        j++;
        if(j>8) break;
        if(k<4) continue;
        i++;
    }
```
ループ本体内に条件分岐式を記述して、while文の判定が成立する前にループを脱出したり(break)、ループの先頭に復帰(continue)してループ本体の処理をスキップさせることができます。

## Re:Mind
```mind:Re:Mind
    ・int i=0
    〇(i<10) の間は繰り返す
        //todo
        □i++
    〇ここまで
```
Re:Mindの前判定繰り返し構文は、最初の〇の後に　「(条件式) の間は繰り返す」を記述し、末尾の〇に「ここまで」を記述します。

```mind:Re:Mind
    ・int i=0
    〇ここから
        //todo
        □i++
    〇(i<10) の間は繰り返す
```
Re:Mindは後判定繰り返し構文をサポートします。その場合、最初の〇の後に「ここから」を記述し、末尾の〇に判定文　「(条件式) の間は繰り返す」を記述します。

```mind:Re:Mind
    ・int i=0
    ・int j=0
    ・int k=0
    〇(i<10) の間は繰り返す
        //todo
        □k++
        □j++
        ◇j>8 の場合
            □脱出する
        ◇ここまで
        ◇k<4 の場合
            □ループ先頭へ
        ◇ここまで
        □i++
    〇ここまで
```
ループ本体内に条件分岐式を記述して、ループ続行の判定が成立する前にループを脱出したり(□脱出する)、ループの先頭に復帰して(□ループ先頭へ)ループ本体の処理をスキップさせることができます。

# おわりに
Re:MindはJavaやC#の経験者向けに設計された日本語プログラミング言語の一種で、ロジック仕様記述言語とトランスコンパイラ言語とで言語仕様を共有しています。ロジック仕様記述言語は疑似言語みたいなものですから、コンパイラを通さないことを前提にするならば未定義の関数を要件表記として使うこともできます。
自然言語の日本語で記述するよりは厳密な構造的な記述が可能です。


[^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)