形式仕様記述では、事前/事後条件、不変条件などを明示的に書き出す必要があるため、自然言語で記述した仕様と比べて、重要な前提条件などが埋もれにくい。チーム内で仕様をもんでいく際も、解釈の差が生じにくく議論がかみ合いやすい。 仕様の解釈の幅はソフトの実装工程において、仕様策定者が想定したのとは異なる動作を作り込んでしまう事態を招きがちだ。こうしたバグは実装担当者による“実装ミス”として片付けられることが多いが、本来は上流工程で仕様を精査し、仕様の品質を高めておけば防げる。形式手法はプロジェクトメンバー間での仕様伝達における、こうした齟齬をできるだけ減らし、ソフト開発をスムーズにするための手法だ。 ライフロボティクスで今回の形式手法導入を主導した同社 研究開発部 部長の川口順央氏は「形式手法を用いることで仕様が安定すれば、以降の作業を見積もりやすい。プロジェクトの見通しが増す効果があったほか、設