形式的な仕様記述がすごいらしい

　早速，メルコ・パワー・システムズの開発部門が原因究明に乗り出す。しかし，いくらデバッグしてみても不具合の原因が分からない。それどころか，現象が非常にまれにしか起きないため，不具合の再現すらおぼつかない状況だった。

　開発作業に暗雲が立ち始めたちょうどその時，社内でモデル検査技術の試験適用を進めていた早水公二氏が現れる。新技術の調査・導入を担当する技術統括部 ビジネスチーム2に所属するモデル検査の専門家だ。既に何件かのプロジェクトでモデル検査の効果に手応えを感じ始めていた同氏は，この不具合の原因究明にもモデル検査技術が使えないかと思い立ち，作業に取り掛かる。そして，モデルの作成やツールによる探索作業などを経た13時間後，見事，不具合の原因を見つけ出したのだった（図2，図3，図4）。

第5回：国内でも成功事例が出現，形式的手法の壁は高くない（2ページ目） | 日経 xTECH（クロステック）

形式的手法を用いることで、再現性が非常に低いバグの原因をわずか13時間で見つけたとな。すごすぎる。

　今回の不具合の要因は結局，境界値に起因する条件判断文の単純な実装ミスだった（図3）。バグというのは，大概が思いも寄らない部分に潜むからこそ，発見できずに不具合となる。レビューやテストの観点を増やせば検出できるという正論だけでは限界がある。「コンピュータのルーチンワークとしてプログラム中を探索するモデル検査は，人力に頼るテストの限界を別の観点から補足してくれるもの」（星野氏）といえる。

第5回：国内でも成功事例が出現，形式的手法の壁は高くない（4ページ目） | 日経 xTECH（クロステック）

形式的な仕様記述は、プログラミング言語とは独立して利用できるのかな。だとしたら、動的な言語においてテストを補完するものになるのだろうか。

　自然言語の仕様であれば，人により解釈は千差万別。一度きりの片方向のやりとりであれば，目立たない仕様解釈の誤差も，仕様精査や実装のサイクルが回る中で蓄積され増幅されてしまうのだった。サイクルを経ても，解釈の誤差が入り込まないような方法論，それが形式的手法だったのだ。「10万行もの仕様をVDMで書いたと言うと，『ほとんど実装に近いですね』などと言われるが，仕様策定者が実装を書いて何が悪いのか。そのくらいの詳細度が本当に必要な立場であれば，実装並みに厳密な仕様でも，ためらいなく書くべきだ」（同社の栗田氏）。

　栗田氏によると，形式的手法による仕様記述を経験すると，仕様を厳密に書く発想が根付くため「今は日本語に戻っても十分厳密に仕様を書く自信がある。形式的仕様記述言語がソフトウエア技術者の共通言語になれば望ましいのでは」とする。

第5回：国内でも成功事例が出現，形式的手法の壁は高くない（5ページ目） | 日経 xTECH（クロステック）

かっこえー！
英語の勉強やめて、仕様記述言語を勉強しようかな。