>>96
習得が大変（つーか普通のプログラマには無理？）なのは事実だと思う。

ただ「実際にプログラム組んでテスト」だと、あくまで有限（一部）の
入力についてしかテストできないけど、ホーア論理とかなら無限（全部）の
入力について検証できる。

だから、「実際にテストするよりも難しい」と直ちに
「形式的仕様検証 ＜＜＜ 実際にテスト」といえるわけでもない。

あと、プログラムの完全な仕様じゃないけど、配列の添え字とか例外処理とか
一部だけ検証するなら、http://research.compaq.com/SRC/esc/みたいな
もっと「お手軽」なアプローチもある。

>>97
数学というか記号論理学と思われ。∀とか∃とか∧とか∨とか¬とか、
そういうの（笑）。