ソフトウェアの信頼性を根本的に高める「形式手法（Formal Method）」の本質

ソフトウェアには自動車や機械をはじめとする他の工業製品と違った特徴がある。「柔軟さ」こそ、それだ。 ところが、柔軟性はＩＴ活用の幅を広げやすくする一方で、ともすればシステムの信頼性や安全性を損なう一因にもなる。 特に高信頼性が求められるシステムでは、柔軟なゆえに可能な場当たり的なコード変更が致命的な障害につながりかねない。 こうした事態を避けるべく、最近にわかに関心が高まっているのが「形式手法（Formal Method）」である。 数学的な記述を伴うので取っつきにくい面はあるが、企業のIT責任者や担当者は、少なくとも本質を理解しておくべきだ。