【形式手法】VDM++を勉強する その1

さて、もうそろそろ大学４回生になり、研究が捗り始める頃ですが、
私に大きな試練が立ちはだかりました。

それが、このVDM++

形式手法に則り開発形式化を検証するのが私の研究テーマなのですが、教授の
「どうせなら今まで使ったことのないような手法（言語）でやってよ＾＾」
という鬼の一言でこのVDM++という言語を用いて研究することになりました。

ですが、自分自身、このVDM++という言語についてよく理解しておらず、
（というか教授から聞くまでその存在すら知らなかった）
今の知識量ではさすがに研究に支障を及ぼすので、勉強しなければ！と思いました。

まぁ、どうせならブログのネタにするかってね

というわけで、VDM++の勉強過程をブログにまとめようと思います。

さて、まずはVDM++とは何ぞや？というところから始めなければいけません。
教授から押し付けられた参考書にはこう書いてありました。

　Vienna Development Method
　1970年代にオーストリアIBMウィーン研究所で開発された形式手法。
　形式仕様記述にカテゴライズされる。
　VDM++はオブジェクト指向に似ており、抽象的な構文を用いてシステムの構造、機能を記述する。

ふむ、なるほど（よくわかってない）
形式手法によってシステムの仕様を書くための言語ってことですね。（多分）



そもそも、ソフトウェア開発の過程はどうなっているのか、見ていきましょう。
ソフトウェアを開発するときには、まず「何をするか」「どうやって実現するか」を
定めることから始まります。
例えば、WSCardDBなら、
What・・・「TCGのWSのカード情報をリスト化し、簡単に検索できるようにする」
How・・・「Visual C#を用いて構築する」
という感じですね。（間違ってるかもしれませんが）

もちろん、設定してからすぐにソフトウェアが完成できるわけではありません。
クラスを作って、メソッドを作って、変数を定義して、処理を作って・・・と
中規模～大規模のシステムだと何ヶ月作業になります。
その過程でできた部品（例えばクラス、メソッド、処理）を中間成果物といいます。

さて、ソフトウェアを開発するフェーズに、なくてはならない作業があります。
それが、テスト作業。

そりゃあ、完成したソフトをテストもなしに公開すると、
思いっきり後悔するハメになりますね！（ﾄﾞﾔｧ...

さて・・・
ソフトウェアのテスト作業にはだいたい2種類のテスト内容に分けられます。
それが「検証」と「妥当性確認」
参考書にはこう書いてありました。

　「検証」
　　成果物が開発者によって定められた基準を満たしているかどうか。
　　「～をすると～が出力される」や「～は～である」等という基準。
　　アプリケーション毎に定まる性質だが、デッドロックしない等、基本的な性質もある。
　「妥当性確認」
　　成果物や正当性の基準がそもそも求めているもの、意図しているものなのか。
　　顧客やユーザー視点から判断される。

ふーむ？
例えば、検証の場合、「1+1=2になってるかどうか、1+1=3とかになってないだろうか」
という、システムの処理的なものに対するテストであり、
妥当性確認の場合、「このソフトウェアって本当にこの機能いるのん？」とか
「（このシステムにはこの機能がついてないと）いかんでしょ」
とかそういう感じのテストってことですね。

このテストという作業、ソフトウェア開発の過程において、どのぐらいのフェーズで
行われるかというと、思いっきり最後の方で行われます。
そりゃ、システムがある程度完成させられないと、テストを行いようがありませんしね。
RTAで例えるとチャートもないのにどの区間が縮むかなーと考えるようなものです。
（ちょっと違うかも）

しかし、テストによってバグやら仕様の誤りやらが発見されると、
ちょっと面倒なことになります。

というのも、モノづくり全てに言えることなのですが、
自分と思い描いてたものと違うものが出来てしまった場合、作り始めなら
簡単に修正を行えるのですが、完成間近になるとそうはいかない。

ちょっと前、ダヴィンチの壁絵を修正しようとして悲惨なことになった
おばちゃんのニュースがありましたね。
誰か始めの方で指摘してあげることができたらあそこまで悲惨なことには
ならなかったのでしょうけれども。

ソフトウェア開発に関しても例外ではなく、
できれば作りながら、それと並行してテストを行いたい、と誰しも思っているわけです。
（後々バグが発見されると修正が面倒なので。誰しも仕事は定時で帰りたいでしょう）



さて、それを可能にするのがこのVDM++という言語、というわけですね。

なんと、この言語、中間成果物を簡単に評価することができるらしいです。
つまり、システム全体は全然作り終わってないけど、途中まであってるかどうか
簡単に確認できるよーってこと。これは嬉しいですね。

また、数ある仕様記述用の言語の中でも、非常に厳格。
日本語が不自由な人が日本語で仕様書を書くと、他の人が見ても全くわからん、
ということになりがちですが、VDMにはその心配がありません。
プログラミング言語と似たような関数や定義を用いることにより、
人による解釈の差異を限りなく小さくすることができるのです。

なるほど！すごいなVDM++！



まぁ、研究以外では間違っても使いませんけどね

今回の勉強内容のまとめはこちら
続きがあるかどうかは私の気分次第ということで・・・