「形式手法」の“論理の力”による開発効率と品質の向上事例

トップエスイーからのアウトカム ～ ソフトウェア工学の現場から 第7回

　社会人エンジニア向けの教育プログラム「トップエスイー」から、エンジニアの皆さんに対して有用な情報をお届けするコーナーです。ところで、形式手法という言葉はご存じでしょうか？ 一般には「数理論理学に基づき、効率よく高品質なソフトウェアを開発するための手法の総称」などといわれます。とはいえ「数理論理学」といわれてもなかなか実感ができないと思います。さらに「総称」と述べましたが、セミナーや書籍などで勉強した方も、その中の一つの手法や観点のみに触れたのではないかと思います。本記事ではAmazon Web ServiceやFacebook等の具体的な事例にも触れ、形式手法と呼ばれるアプローチのいくつかの方向性・可能性について紹介します。「形式手法」という広すぎる言葉はいったん忘れて、難しい専門用語に振り回されないよう、できるだけ一般的な言葉での説明を補足します。