仕様記述言語VDMというのを習っています。
仕様を書く言語というのがあったのは初めて知りました。。
仕様って、がりがり日本語で書いていくもんじゃなかったっけ?

UMLとか言語で書かないツール類もありますが、このVDMというものはまさにプログラミング言語と同じ。。
オブジェクト指向でかけるそうです。

使っているツールが、EclipseベースのOvertureと言うもの。言語の使用自体は、プログラミング言語とはちょっと違った感じで、集合とかを直接扱えるので普通のプログラミング言語のつもりで挑むと、ハマります。

ちゃんとテストユニットもあるので、プログラムできる人だと違和感ないと思います。
ただ、いわゆる「SE」と呼ばれる人が、日本では仕様書を作ったりしますが、その人達がこのVDMと言うものを使いこなせるわけもなく、当然のように全く普及が進んでいないというのが現状でしょう。

仕様記述言語は仕様上の不具合をなくすという意味であるわけですが、これが、機械的にチェックできるというところが非常に素晴らしいのではないでしょうか?

因みにおサイフケータイのフェリカのプロジェクトでこのVDMが使われたそうです。
もっと普及すればいいのではないでしょうか?

ただ、使いこなすには集合論などの数学の知識が必要になりますので、文系出身のSEさんには辛いでしょう。