自動改札機の運賃計算プログラムはいかにデバッグされているのか？

http://www.publickey1.jp/blog/12/_1040.html
興味深く読んだ。
特に、「現実には全パターンはできない」とスタンスを明確にしているので、こういう話が出てくる。

こうやって網羅的なものから絞り込んでいくことのいいところは、テストできていないのがどこなのか、分かっているということです。

諦める場所を明確にすることで守る場所を明確にということか。
他にも、仕様記述を形式化することで試験抽出に役立てるとか、というのは目から鱗だった（常識なのだろうか？）