>>123
「だったら」が何を指すのか意味不明だし、また静的解析みたいな曖昧な言葉を持ち出す

まだ >>123 は(言語としての) VDM における検証や証明を扱うレベルに達していないので、
無理に背伸びはせず(処理系としての) VDM Tools を触ることから始めたほうがいいと思われ
ただし、今のままでは軽量と言われる VDM Tools ですら理解するのは難しいと思うがね