はじめに

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

この記事内容の作業目的

VDM++の下記の制御構文³⁴についていくつかの記事に分割して比較検討します。クラスの定義構文についてはこちらの記事⁵を参照することができます。

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

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

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

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

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

この記事内容の保証

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

構文比較

VDM++

    doAnything: () ==> int
    doAnything() ==
    (
       --todo1
       return i;
    )

VDM++

    doAnything: () ==> ()
    doAnything() ==
    (
       --todo1
       return
    );

VDM++のreturn文は操作定義ブロック文内の式の値を戻します。変数や値を返さない場合はその時点でブロック文の実行を終了します。
VDM++のブロック文は()で囲われた範囲となります。セミコロンによる構文の終端ですが、ブロック文の末尾の行の終端は省略可能（下段のようなイメージ。上段のようにつけてもツールによってはエラーとならない）。定義ブロック文の終端にも下段イメージのように終端は必要。

Java

    int doAnything()
    {
       int i = 1;
       //todo1
       return i;
    }

Java

    void doAnything()
    {
       //todo1
       return;
    }

Javaのreturn文は関数定義ブロック文内の式の値を戻します。変数や値を返さない場合はその時点でブロック文の実行を終了します。
Javaのブロック文は{}で囲われた範囲となります。

C#

    int doAnything()
    {
       int i = 1;
       //todo1
       return i;
    }

    void doAnything()
    {
       //todo1
       return;
    }

C#のreturn文は関数定義ブロック文内の式の値を戻します。変数や値を返さない場合はその時点でブロック文の実行を終了します。
C#のブロック文は{}で囲われた範囲となります。

Re:Mind

    ▽int doAnything()
        ・int i = 1
        //todo1
        □返す i
    △

Re:Mind

    ▽void doAnything()
        //todo1
        □返す
    △

Re:Mindの返す文は関数定義ブロック文内の式の値を戻します。変数や値を返さない場合はその時点でブロック文の実行を終了します。
Re:Mindのブロック文は▽の定義行の末尾から△で囲われた範囲となります

おわりに

いかがでしたでしょうか？VDM++にもreturn文があるのですね。アルゴリズムの陰定義のイメージが強いVDM++ですが、普通にロジックは組めそうですね。
VDM++でロジックまで書いた場合、実装用のプログラミング言語のソースコードにどのように反映させるかが問題です。

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

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

はじめに

この記事内容の作業目的

この記事内容の保証

構文比較

VDM++

Java

C#

Re:Mind

おわりに