最近訳あって形式手法(Formal Method)を勉強している。形式手法とは数学的な考え方（数理論理学）をソフト開発やハード開発に持ち込み信頼性を確保する手法の総称。形式手法の歴史は長いが一部の人にしか知られてないと思う。
その中でも比較的取っつきやすいのが厳密さより実効性を優先するライトウェイトと呼ばれる手法であり、VDMはIBMが開発したその１つ。VDMには表現するモデルに対応してVDM-SL、VDM++、VDM-RTの3つの記述言語があり、最初のVSM-SLはISO規格にもなっている。VDM自体はロジックの記述に使えるが手足がほとんどない。数学の清い世界にI/O等の泥臭い話は馴染みにくい事は理解できる。でも実用に使うにはI/O等は避けて通れない。
VDMの開発環境としてEclipseの上に構築されたOvertureがフリーで使える。つまりVDMはJAVA-VMのバイトコードにコンパイルできる。守備範囲の広いJAVAと繋げて使うこともできるようだ。・・・このやり方はOverture User Guideの中に書いてあるがイマイチ分からなかった。
VDMとJAVAでは表現できる世界や規格の決め方が異なるから単純に繋げられないことはわかる。例えばJAVAの整数(long)に対応するVDMのデータ型には整数、自然数（2種類）の3種類ある。文字列の表現がVDMでは３通り可能・・・ってな具合。
結論から言うとVDMからJAVAを呼び出す場合と、その逆でやり方が全く異なった。これを解説すると長くなるから別の機会に。
・・・とりあえず
