HOME > 研究活動・産学官連携 > ネットジャーナル > ネットジャーナル33

ネットジャーナル33

帰納的定理証明によるソフトウェアの検証

――他にはどのような研究がおこなわれているのですか。

博士(工学)栗原 正仁 教授栗原 先ほどもお話したようにソフトウェア工学はソフトウェアを効率よく確実に開発する技術であり、人命や財産に関わるシステムなどはプログラムの「正しさ」が極めて重要です。そのため、実際に動かしてみて期待通りの動作をするか、安全であるかなどのテストをするのですが、すべての状況をもれなくテストすることはほぼ不可能で、部分的な正しさを確認するテストを行うのが一般的です。時折、大規模システムのトラブルなどがニュースになるのも、テストでは検証しきれなかった事態が起きたためです。

テストよりも一歩進んだ検証の手法として「定理証明」があります。もともとは数学の世界で数式の正しさを証明するものですが、これをプログラムに当てはめ、数式と同じようにプログラムの正しさを証明しようというのがソフトウェア工学における定理証明です。

そのためには、ソースコードを数学のように扱える形式に書き換える必要があり、さらにそれをコンピュータで計算できるようにしなければなりません。数学の定理をコンピュータで証明することは人工知能の分野で50年以上前から研究が行われていて、ここでもソフトウェア工学と人工知能技術の融合が新たな可能性をもたらしています。

一般的なプログラムは、例えばJavaのように、英語によく似た単語が使われており数式とはかけ離れています。このままでは定理証明には使えないので、本研究室では、数式に近い関数型プログラミング言語(解説2)をベースにした「項書換え系(解説3)」という疑似的なプログラミング言語によってプログラムを記述します。その上で、プログラムが満たすべき性質を、数学的帰納法(解説4)によってコンピュータで自動的に証明し、ソフトウェアの性質や正しさの検証を行います。

項書換え系のプログラミング言語で記述されたプログラムの性質を、数式の帰納的定理と同じような方法で記述し、それをコンピュータで自動証明する。それが本研究の重要なポイントです。現段階では、ソフトウェア全体を完全に保証するわけではありませんが、定理証明によって裏付けられた部分は自信を持って「正しい」と言うことができます。現代社会では、ソフトウェアの品質を客観的に評価することがますます重要視されており、定理証明によるソフトウェアの検証はソフトウェア開発にとって不可欠な技術になると考えられます。また、関数型プログラミング言語や定理証明の知識・技術をもった人材の必要性も高まると予想され、大学における教育にも力を入れていきたいと思います。

(2014/09/25)

ページの先頭へ