『科学的モデリング』による≪Refinement≫と≪Validation≫

上位モデルから下位モデルへの正しい作業を少しでも数学的(形式的)に実施するための具体的な方法の整理をしている。
　
雑駁に言ってしまえば≪Refinement≫と≪Validation≫。
　
かなり厳密な方法は開発現場に導入するには無理があるから、半形式的にならざる負えないが、それでも格段に生産性と品質が向上する。
　
一方で、現在のMDAは、形式的なRefinementの考え方がごっそり欠落しているものが多く、これでは単にツールによる自動化の手間しかメリットが得られない。既にある殆んどのMDA方法論はこのタイプだ。
　
これでは意味が無い。
　
Refinementにも垂直(Vertical)と水平(Horizontal)があるが、理想はなるべく垂直Refinementにしたいところだが、現実の現場の都合やプログラム言語の機能を考えると水平Refinementの性質が強くなるだろう。
　
ごく簡単な仕様とUMLクラスと妥当性のシナリオを用いて、幾つかの仕様記述言語による比較と考察を行う。
　
関連のナビゲーションは相手先のインスタンスあるいはインスタンスの集合が存在しない場合は、OCLやVDM++は、undefinedが∅が返されるが、Alloyにはこの区別がない。つまり部分関数の述語(早い話が関連や演算)の考え方にも違いがある。
　
クリーネ論理系(Kleene Logic)の3値論理の取り扱いも、OCLやVDM++は『強い論理』を採用している。