IPA (独)情報処理推進機構の「厳密な仕様記述入門」を読み解く - 要求仕様 形式記述言語VDM/VDM++

# はじめに
システム開発におけるいわゆる下流工程の開発（実装・製造ともいう）現場においては、現在（21世紀第1四半期）英字を使った実装言語（プログラミング言語）が主流で、コメント部分以外への日本語の記述への抵抗は大きいようです。

そこで上流工程ではどの程度日本語が使われているのかを調査するため、ちょっと工程上の位置づけは内部設計の上になりますが、要求仕様記述段階での使用が想定されているVDM(Vienna Development Method)[^1]の具体的な記述例としてIPA (独)情報処理推進機構の「厳密な仕様記述入門」を拝読しました。

## 対象読者
システムエンジニアさん。エンベデッド系やネットワーク・インフラエンジニアもシステムエンジニアさんですが、狭くは業務系システムの設計に携わる方がいいな。

# 厳密な仕様記述とは
VDM/VDM++のような形式記述言語を使って要求仕様を書きましょうという意味です。
「厳密な仕様記述入門」PDFは下記のIPAアーカイブのリンクからオープンにダウンロードして閲覧できます。全5章からなり205ページあります。つまみ読み可とありますが、「要求」と「仕様」と「設計」の本文書上の定義は確認しておいた方がよいです。

[[PDF] 厳密な仕様記述入門 - IPA 独立行政法人 情報処理推進機構 2013/3
](https://www.ipa.go.jp/archive/digital/iot-en-ci/keishikisyuho/hjuojm000000m6wx-att/000026829.pdf)

# 設計とは
「設計」という用語はいろいろな業界で使われていて、アプリケーション開発やシステム開発でも使われていますが、ハードウェア・エンジニアが前身の私は、ソフトウェア業界の「設計」にまつわるイメージは大きく異なっていると、この業界に入ったとき感じました。もしかしたら、システム開発だけでアプリケーション開発は別のような気がしますが、製品企画段階の課題も「設計」と称している場合があって紛らわしいです。

本PDFでは「仕様」と「設計」をこの２単語で区別していて、「仕様」は要件定義や要求仕様の策定工程、「設計」は、内部設計、詳細設計と実装（システム業界では製造ともいう、アプリケーション業界の製造は通常CDプレスなどメディア生産と認識していましたが、昨今のダウンロード提供の実勢からすると別の言い方になっているかも）を合わせています。

「設計」が本書ではほぼ実装の一部という扱いなのは、本書の主題が要求仕様の策定、定義（と形式言語を使うことによる機械的な妥当性、正当性の検証）を行うことを主題としているため、主題外のためざっくりしているせいと推察しています。

# 仕様とは
本PDFでは、ソフトウェア化対象の課題を、問題を解決したい世界における「事実」と「願望」で構成されているものとします。「課題」の中から、解決されることによって生み出される「価値」を、さらに実際にその「価値」を生み出すためのソフトウェアの性質を定義したものが「仕様」だとしています。このあたりは要件定義や要求仕様の策定が成功した場合のイメージとも言えますね。

「仕様」は要件定義や要求仕様の策定工程で、その記述に数学的形式記述言語VDM（とそのオブジェクト指向拡張のVDM++）を使いましょうという導入ガイドに本PDFはなっています。ですので、アルゴリズムやロジックの記述はなく、ソフトウェア化対象の事象の定義や入力と出力の定義といった範疇となります。

# 要求とは
「要求」は前記の「課題」に含まれる「事実」と「願望」のうち、後者に含まれるものの１つと位置付けています。
>「願望」には「要求」「提案」「企画」といったこれから実現したい要素などが含まれています。

要件定義の中の構成情報といった位置づけでしょうか。システム開発業界には、ウォーターフォール的な工程のネーミングに、要件定義、外部設計（要求仕様作成、画面イメージの外見、データマッピング）、内部設計（構造・状態などに加えてデータの型、ロジック・アルゴリズムなど実現仕様の策定）があって、これらを総称して「設計」と言っている場合があります。

体力のある大企業さんのユーザー企業ですと、プロポーサルリクエスト（Request For Proposal RFP）として実現したい課題をある程度まとめてシステム会社さんに提示してくれるので、楽な場合があります。ただし競合に勝つためには、RFPの上を行くといったことが営業的には要求されます。


# 要求仕様形式記述言語VDM/VDM++の記述例
この大見出しの内容とはそぐわないのですが、実は本記事は形式記述言語VDM/VDM++の記述ルールの紹介といったものではなく、その中でどの程度日本語が使われているのかなというのが調査目的でした。

具体的な記述の詳細はこちらのサイトからツールとサンプルをダウンロードして書いてしまった方が速いかもしれません。

https://research.nii.ac.jp/~f-ishikawa/vdm/index.html

PDFの本文中、興味深かったのは、下記の数学・論理学上の論理記号と、自然言語の日本語表記、自然言語の英語表記と、VDMトークンとの対応表でした。

>表 2-1 : 論理記号と自然言語と形式仕様記述言語の対応

|論理記号|日本語|英語|VDM|
|:-:|:-:|:-:|:-:|
| ¬  | でない/以外  |  not | not |
| ∧ | かつ/及び/さらに/と/,| and | and |
| ∨ |  または/あるいは/や/か/,  | or | or |
| ⇒ | ならば/のとき/とすると  | implies<br/>then  | => |
| ⇔ | ならば/同値/つまり/<br/>言い換えると  | if and only if<br/>equivalent  |<=>|
| ∃x |ある/存在する | there exists x such that | exists x  |
| ∀x  |すべての/必ず/任意の| for all x ...   |   forall x |


論理記号に対応する日本語の同意異語ってけっこうたくさんあるのですね。また、論理記号のターンEやターンAは久しぶりに変換しました。∀は「ターンエー」で変換できるのですが、∃は「ターンイー」では変換できず、「そんざいげんていし」で変換しました。

本PDF本文P49の
>**指示と定義と論理式**
どのような手法を使うにせよ、自然言語による記述も含めて開発文書の中では「指示 -
designation」と「定義 - definition」の区別をはっきりさせなければなりません。

の記述で「指示」[^2]　は私としては重要なパワーワードと認識しました。

この「指示」と「定義」を使って別の「定義」を再定義することに、ForthやMind[^3] の世界に近いものを感じるのは、私がMindユーザーだからで、他の人は恐らくそのような連想はないものと推察されます。

>結局「指示」も「定義」も形式仕様記述言語の世界では「型」や「関数」を組み合わせて表現されることになります。

ここからの形式表現はオブジェクト指向プログラミング言語のクラス定義や、構造化プログラミング言語の構造体定義、関数表記の手続き型プログラミング言語C/C++/Java/C#に近いものを感じます。

>図 2-13 型の定義

```mind:VDM
public 文字列型 = seq of char;
public 日付型 = int;
public 性別型 = <男>|<女>;

public 人型::
	名前:文字列型
	誕生日:日付型
	性:性別型
	父親:[人型]
	母親:[人型];
```
父親、母親の人型が[]で囲われているのは人型または未定義(nil)という意味です。血縁関係ではなく戸籍上の関係を表しているようです。
>図 2-14 基礎的な関数の定義 （一部、親子のみ）
```mind:VDM
public 親子? : 人型 * 人型 -> bool
親子?(p,c) == (p=c.父親) or (p=c.母親);
```
これは、親子関係の判定関数の引数が、人型のpと人型のcを与えると、cの父親がpに等しい、またはcの母親がpに等しい、ならば、真を、いずも等しくない場合は偽を返す　といったことが定義されています。引数名の意味としては、pはパレント、cはチャイルドと言ったニュアンスなんでしょうね。

>図 2-15 親の集合を求める関数
```mind:VDM
public 親 : 人型  -> set of 人型
親(x) == {x.父親,x.母親}/{nil};
```
人型xを渡すとxの両親のオブジェクト配列を返すイメージ。/{nil}は未定義要素を除くの意。ひとり親家庭の場合はいずれかの要素で要素数１のオブジェクト配列を返す感じ。

>付録2 例題ファイル （一部、血縁クラスのみ、メソッド一部に限定）
```mind:VDM++
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のオブジェクト指向拡張のVDM++によるクラス定義例です。typesとfunctionsでデータ型とメソッドを分けているのが特徴的ですね。

実現方法はこの工程では対象外なので、ある意味**インターフェースだけ書いて実装は書かないオブジェクト指向プログラミング言語っぽいもの**と認識しました。といっても論理的なルールはある程度記述するようですね。

本PDF本文P64に
>**形式仕様記述言語で文の曖昧さを取り除く**
さて、改めて通常の日本語表記の曖昧さを考えてみましょう。

と書かれているのですが、ここでは当然、自然言語の日本語表記との比較で形式記述言語の厳密さを訴求されていらっしゃいます。この著者の学者さんは恐らく形式的実装記述言語の日本語プログラミング言語のことは認識されておらず、もしもここで、自然言語の日本語ではなく、日本語プログラミング言語で記述したとしたら、曖昧さもなく論理的算術式的な記法を手順的な記法にすることで、もう少し直感的にわかりやすくなる余地があるような気がしました。

# おわりに
本PDF中のVDM/VDM++の論理式、型定義、関数定義では日本語のオブジェクト名が多用されていました。実際のツール処理系が日本語を処理できるのか、本PDFではわかりやすさのためにあえて推奨はしないが日本語を使っているのかは、本PDFからは読み取れませんでした。

ただ、上流工程としてはユビキタス言語などの辞書リストが国内向け案件の場合は日本語で書かれている場合が多いと推察されますので、要件定義段階での形式言語を導入した場合、トークンが英字でもオブジェクト名や関数名は日本字のまま表記される可能性は高いと思われました。

VDM/VDM++が一般的に導入されるようになり、型定義、関数定義では日本語が記述されている場合、実装のロジックまでを記述する日本語ロジック仕様記述言語[^4]　との親和性は高いかもしれません。日本語ロジック仕様記述言語は日本語トランスコンパイラ言語と段階的詳細化という形で連携できれば、ソフトウェア開発の生産性と（上流からの）正当性を向上できる可能性はあるように感じました。

## 2023/10/11 追記
PDFの末尾に各形式言語別ツール別の日本語識別子の対応状況が記されていました。VDM/VDM++はZ言語などに比べて日本語識別子の対応が柔軟そうです。

### VSCode対応ツール
このPDFの発行日が2013年3月でVDM/VDM++対応ツールには記載がありませんが、VSCode拡張はやはり存在するようです。

https://marketplace.visualstudio.com/items?itemName=korosuke613.vdmpp-extension

https://marketplace.visualstudio.com/items?itemName=overturetool.vdm-vscode


[^1]: IBMのウィーン研究所で1960年代から70年代にかけて開発された形式手法。Vienna Development Methodを直訳すると「ウィーンの開発手法」といった感じ。Viennaにひっかけた何か他に他意があるかは未確認。
[^2]: 「指示」とは現実世界との直接的な対応関係を表す「用語」を意味する。引用PDFよりP50。
[^3]: 一般にForth系とされる日本語プログラミング言語
[^4]: Qiita [オープンな設計言語仕様 日本語ロジック仕様記述言語 Re:Mind（リマインド）](https://qiita.com/mylifewithviolin/items/52f806777e6ea031de94) 参照