ソフトウェアの品質と安全性向上のための「形式手法」入門編

　ソフトウェアの品質を確保するため、誰もがレビューとテストを行う。しかし、一般的に行われているレビューやテストにおいて、システムが正しく動作することをどの程度保証できているのだろうか。

　優秀なエンジニアによる小規模ソフトウェア開発であれば、設計・テスト・検証における細心の注意とノウハウにより高品質のシステムを実現することが可能だ。では、たとえば50人を超えるようなチームではどうだろう。

　システムの大規模化・複雑化から、上流工程での品質改善手段が求められている。こうしたソフトウェアの品質と安全性向上のために、「プログラムの正しさ」に関する研究から生まれたのが「形式手法（Formal Method）」だ。今回は、厳密な仕様定義を目的とした「形式仕様記述」を中心に分かりやすく解説する。