はじめに
形式記述言語VDM1 のオブジェクト指向拡張のVDM++による構文をIPAの導入書2 で見た感じ、ある意味インターフェースだけ書いて実装は書かないオブジェクト指向プログラミング言語っぽいものと認識しました。といっても論理的なルールはある程度記述できるようです。逆に記述もできてしまうので、要求仕様の記述として書きすぎないようにするルールづくりが必要のようです。
この記事内容の作業目的
そこで内部仕様の記述用に設計したロジック仕様記述言語 Re:Mind（リマインド）3 と代表的な構文を比較して、Re:Mindが要求仕様記述用途で使用できるか、不足する言語仕様要件はなにかといった点を検討してみます。
この記事内容の保証
※この記事には仕様的な情報が含まれます。各言語で書かれた引用ソースの妥当性は保証されません。また、自作言語は開発中（試作段階）のため、本記事に開示された仕様は予告なく変更される場合があります。
VDM/VDM++の構文はIPAの導入書から引用しています。「図 2-13」といった記述は導入書の記述に準じています。
型の定義
下記はVDMによる型の再定義と列挙体、構造体に相当する型の定義記述の例です。これをRe:Mindの構文で書き換えてみます。
図 2-13 型の定義
public 文字列型 = seq of char;
public 日付型 = int;
public 性別型 = <男>|<女>;
public 人型::
名前:文字列型
誕生日:日付型
性:性別型
父親:[人型]
母親:[人型];
父親、母親の人型が[]で囲われているのは人型または未定義(nil)という意味です。血縁関係ではなく戸籍上の関係を表しているようです。
▽public 列挙体 性別
男,
女
△
▽public 構造体 人型
・String 名前
・Date 誕生日
・性別 性
・人型? 父親
・人型? 父親
△
ロジック仕様記述言語 Re:Mind（リマインド）はJavaやC#などC/C++言語仕様を継承したオブジェクト指向言語の経験者向けに設計された日本語トランスコンパイラ言語 Re:Mindのサブセットとして、制御構文の開始シンボルとして、◇、〇、□、・などの全角記号を用い、箇条書きされた日本文としての体裁を共有していますが、基本型は日本字で書いても英字で書いても可としています。人型?の?はC#のNULL許容値型と同意です。
関数の定義
下記はVDMによる関数の定義の記述の例です。これをRe:Mindの構文で書き換えてみます。
図 2-14 基礎的な関数の定義 （一部、親子のみ）
public 親子? : 人型 * 人型 -> bool
親子?(p,c) == (p=c.父親) or (p=c.母親);
これは、親子関係の判定関数の引数が、人型のpと人型のcを与えると、cの父親がpに等しい、またはcの母親がpに等しい、ならば、真を、いずも等しくない場合は偽を返す といったことが定義されています。親子?の?はbool値を返す関数の意。
▽public bool 親子関係を判定する(人型 親,人型 子)
◇親 == 子.父親 || 親 == 子.母親 の場合
□trueを 返す
◇他に
□falseを 返す
◇ここまで
△
Re:Mindで書き換えるといまのところ手順的な記法しかないため、論理式だけで書かれたVDMに比べて冗長にはなりますね。
図 2-15 親の集合を求める関数
public 親 : 人型 -> set of 人型
親(x) == {x.父親,x.母親}/{nil};
人型xを渡すとxの両親のオブジェクト配列を返すイメージ。/{nil}は未定義要素を除くの意。ひとり親家庭の場合はいずれかの要素で要素数１のオブジェクト配列を返す感じ。
▽public 人型[] 親を取得する(人型 子)
・人型[] 両親
◇子.父親 != null & 子.母親 != null の場合
□両親=初期化 人型[2]{子.父親,子.母親}
◇他に 子.父親 != null & 子.母親 == null の場合
□両親=初期化 人型[1]{子.父親}
◇他に
□両親=初期化 人型[1]{子.母親}
◇ここまで
□両親を 返す
△
一般的なプログラミング言語の記述量と大きくは異ならないと思いますが、手順的な記述ですとやはり長くはなりますね。ラムダ式を導入している言語の気持ちがわかるような。Re:Mindの記述の場合、子.父親と子.母親が両方nullだった場合、要素１で値nullの人型配列が返るとしています。
クラスの定義
下記はVDM++によるクラスの定義の記述の例です。これをRe:Mindの構文で書き換えてみます。継承はどちらの言語でも記述できますが、今回は例題的に継承無しの例となります。
付録2 例題ファイル （一部、血縁クラスのみ、メソッド一部に限定）
class 血縁
types
public 文字列型 = seq of char;
public 日付型 = int;
public 性別型 = <男>|<女>;
public 人型 :: 名前 : 文字列型
誕生日 : 日付型
性 : 性別型
父親 : [人型]
母親 : [人型];
functions
public 親 : 人型 -> set of 人型
親(x) == {x.父親, x.母親}¥{nil};
public 親子？ : 人型 * 人型 -> bool
親子？(p, c) == (p = c.父親) or (p = c.母親);
end 血縁
VDM++によるクラス定義例です。typesとfunctionsでデータ型とメソッドを分けているのが特徴的です。
▽class 血縁
▽public 列挙体 性別
男,
女
△
▽public 構造体 人型
・String 名前
・Date 誕生日
・性別 性
・人型? 父親
・人型? 父親
△
▽public bool 親子関係を判定する(人型 親,人型 子)
◇親 == 子.父親 || 親 == 子.母親 の場合
□trueを 返す
◇他に
□falseを 返す
◇ここまで
△
▽public 人型[] 親を取得する(人型 子)
・人型[] 両親
◇子.父親 != null & 子.母親 != null の場合
□両親=初期化 人型[2]{子.父親,子.母親}
◇他に 子.父親 != null & 子.母親 == null の場合
□両親=初期化 人型[1]{子.父親}
◇他に
□両親=初期化 人型[1]{子.母親}
◇ここまで
□両親を 返す
△
△
Re:Mindは基本的な型の変数の宣言は中点・で関数定義とは区別しやすいのですが、列挙体や構造体、そしてクラス定義となると関数定義の開始記号▽と同じなので、ぱっと見は区別しにくくなります。中かっこがついていると関数定義みたいなことになります。
▽class 血縁
▽public 列挙体 性別
男,
女
△
▽public 構造体 人型
・String 名前
・Date 誕生日
・性別 性
・人型? 父親
・人型? 父親
△
▽public bool 親子関係を判定する(人型 親,人型 子)
//未定義
△
▽public 人型[] 親を取得する(人型 子)
//未定義
△
△
制約条件の記述をどうするかはさておき、ある意味インターフェースだけ書いて実装は書かないオブジェクト指向プログラミング言語っぽいものとしてみると、上記のような記述状態もあってもよいような気がしてきました。（UMLのクラス図が書けるレベル）
おわりに
形式記述言語VDM++では関数の定義が、通常手順的に書かれるよりは数式っぽい形式の記法に寄せることで、だいぶ短く記述できることがわかりました。
記述量が多くなってくると、数式っぽい形式の意味がぱっとわかるようであれば、そちらのが全体認識の効率はよさそうですね。
要求仕様の記述内容として、形式記述言語VDM++ではどの程度の内容を書くのが標準的なのかとはまだわかっていませんので、もう少し構造化手順よりの構文（Re:Mindの◇、一般的にはif文switch文、Re:Mindの〇、一般的にはforループ）をVDM++ではどのように使っているのかを調べてみます。
-
IBMのウィーン研究所で1960年代から70年代にかけて開発された形式手法。Vienna Development Methodを直訳すると「ウィーンの開発手法」といった感じ。 ↩