漏れはおおざっぱにいって
「形式仕様記述」⊃「プログラム言語の仕様記述」
「形式仕様記述」⊃「モデルチェッキングを使った機能検証」⊃「等価性チェック」
だと思った。モデル検査をするには満たすべき性質（＝仕様）を与えないといけないし、
等価性チェックをするにも等価になるべき相手（＝仕様）を与えないといけないし。
87は何か特定の種類の「仕様記述」が念頭にあったと思われ。