形式手法

日経コンピューターNo.657(2006.7.24)の特集2「バグ・ゼロを目指す『形式手法』」を読みました。

これまで形式手法と言われてもなかなかピンとこなかったのですが、システムを状態遷移マシンとみなして各状態の事前条件と事後条件を明記し、（ツールで）遷移全体で矛盾がないか検証する、ということらしくて（誤解してたらすみません）、なんとなくちょっと分ったような気がします。
難しい・大変、に対する解決として、UML等から変換生成することに加え、Java Modeling Language(JML)、JBehave、SPEC#等の既存言語の拡張を用いることで、徐々に普及してきていると。そうですか。

しかしスペックの記述は形式手法？このあたりは新たな謎。