現在の私たちの身の回りでは様々なコンピュータが動作しています。例えば、航空機の管制システムや銀行のオンラインシステム、自動車や家電、そしてゲーム機やスマートフォンなど、たくさんのコンピュータが私たちの生活を支えています。これらのコンピュータの中ではソフトウェアが動作してコンピュータを制御しています。

ソフトウェアの開発では、人間が考える「コンピュータにこんなことをしてほしい」を「コンピュータがするべき動作」に変換し、その「するべき動作」を「プログラム」として記述します。この過程は一種の翻訳であると考えることができます。コンピュータの動作はソフトウェアによって決まるので、ソフトウェアが正しく作られていることは非常に重要ですが、様々な理由により翻訳の過程で誤りが入り込みます。この誤りがいわゆるバグであり、ソフトウェアの期待しない動作につながります。

ソフトウェアに入り込んだ誤りを見つけるために一般には「テスト」が行われます。テストでは、実際にソフトウェアを動作させ、何らかの操作をしたりデータを与えたりして期待通りに動作するか確認します。期待通りに動作しなければ誤りが残っていることがわかります。ただし、テストの時に期待通りに動作したからといっていつでも正しく動作するかどうかはわかりません。一方、数学レベルの厳密さでソフトウェアの正しさを検証する技術の研究も行われています。実際のソフトウェア開発で用いるにはいくつかのハードルを乗り越える必要があるので実用された例は現時点では少ないですが、この技術を用いることで、どのような入力が与えられてもソフトウェアが正しく動作することを保証できます。

私の現在の研究テーマの1つに「情報流解析」があります。情報流解析は、クレジットカード番号のような機密データを扱うソフトウェアが機密データに関する情報を漏らす可能性がないか、ソフトウェアのプログラムを解析して判定する技術です。ここでは、「機密データに関する情報を漏らさないこと」をソフトウェアの正しい動作だと考え、常に正しく動作することを数学レベルの厳密さで保証することを目指しています。

ソフトウェアの正しさをどのように定義しどのように保証するか、その観点も方法もさまざまであり、一筋縄で解決できる問題ではありません。しかし、私たちの生活がソフトウェアに支えられており、ソフトウェアの不具合によって大小さまざまな影響を受ける以上、ソフトウェアの正しさを保証すること、そして正しいソフトウェアをうまく開発できるようにすることはとても重要なことです。