基幹理工学部 情報理工学科 寺内多智弘

現在、コンピュータソフトウェアは社会生活のいたるところに使われています。例えば、自動改札機や銀行ATMなど身近な日常生活の機器も、旅客機のフライトコントロールや放射線治療機器など命に係わる機器もソフトウェアプログラムで動いています。また、スマホアプリや、私が今この文章を書くために用いているワードプロセッサもすべてソフトウェアプログラムです。同時に、プログラムは基本的に人が書くものなため誤りを含むことも多く、プログラムの不具合は大きな社会的課題となっています。不具合のない「正しいプログラム」を作るにはどうすればよいのでしょうか？

プログラムの不具合を防ぐ手段は様々な角度から研究されています。その一つが、プログラムの正しさをコンピュータアルゴリズムにより検証しようという「プログラム検証」です。つまり、「プログラムの正しさ検証するプログラムを作ろう」という試みです。コンピュータサイエンスの父と呼ばれるアラン・チューリングもプログラム検証についての論文を執筆したなど、プログラム検証の歴史は古く、コンピュータサイエンス分野草創期から考えられていたテーマです。より近年では、マイクロソフト社創業者であるビル・ゲイツ氏が「プログラム検証はコンピュータサイエンスにおける至高の目標（holy grail）である」と発言するなど話題を集めました。

プログラム検証は、プログラムが設計者の意図（仕様）通りに動作することを検証します。様々なプログラムと仕様が考えられますが、ごく単純な仕様の検証も計算理論的に非常に困難な問題になります。例えば、チューリングマシンで記述可能な任意のプログラムを対象とした場合、（自明でない）仕様の検証はすべて決定不可能な問題です。現実のプログラミング言語は事実上すべてチューリング完全なため「プログラム検証は理論的に不可能！」ということになります。このため、プログラム検証の研究は、真っ向勝負ではどうにもならない難しい問題に対し、うまい切り口を見つけることで完全ではないが多くの場合有効な手法を得ることが鍵となります。

考え方の一つに、対象プログラムを部分的に抽象化し、元のプログラムより多くの動作するが解析可能な形にみなす、というアイデアがあります。これは、安全性仕様と呼ばれる「実行中に悪いことが起こきない」という形の仕様の検証に有効なアイデアです。実際より多くの動作をする抽象化されたプログラムが悪い動作を起こさないのならば、元のプログラムもそうだからです。粗すぎない適切な抽象をどう得るか、また、抽象化されたプログラムをどう効率よく解析・検証するかなどの課題は自明でなく現在も盛んに研究が行われています。

上記のような課題およびプログラム検証研究全般に大きく関わるのが、定理証明・型システムなど、数理論理など数学基礎論や理論計算機科学の概念です。プログラム検証は、「正しさ」を求めるというその性質ゆえ、曖昧さのない明確な理論的体系で議論する必要があるからです。例えば、SATソルバ・SMTソルバという複雑な数理論理式の真偽性を高速に判定する定理証明技術がここ10数年で急速に発展し、近年のプログラム検証はその恩恵を大きく受けています。これらは、その圧倒的な有用性ゆえdisruptive technology（破壊的技術）とも呼ばれ、プログラム検証を含むさまざまな科学技術の分野に大きな影響を与えています。また、逆に、ウェブプログラムのセキュリティ性質の検証が文字列に関する述語論理のための定理証明技術の発展を促すなど、プログラム検証研究と定理証明研究の間での双方向の貢献も盛んに起こっています。コンピュータソフトウェアの正しさという実用面と数理論理・計算理論など理論面の両方を持つことが、プログラム検証研究の大きな醍醐味です。