研究 / Research

バグのないソフトウェアをめざす

　プログラミング言語理論は、プログラミング言語（FortranやCOBOL、C、Python等）の意味や計算モデルを研究する学問です。仕事や社会に役立つソフトウェアを直接実装するわけではありませんが、バグ（欠陥）のない正しいソフトウェアを書くにはどうしたらいいのかといった、ソフトウェアが重要な位置を占める現代社会では大きなインパクトにつながる研究です。

　ソフトウェアのバグ撲滅は大きな課題ですが、かなり難しいのが実情です。プログラミング言語理論の研究は数学的道具を使って行なわれますが、バグの定義とプログラムはどう動くべきかという定義が難しく、また、定義できたとしても、与えられた定義に従ってプログラムが正しく動作しているかを検証することは更に困難です。

ソフトウェアのバグ検出の方法

　プログラムのバグを検出する方法の一つに、式に様々な型を割り当てて値が正しく使われているかどうかを検査する型システムがあります。私のこれまでの研究では、動的型付け^*1と静的型付け^*2を組み合わせることで、プログラムのバグをできるだけ検出しつつ容易で迅速に使える検証システムの研究を行ってきました。

　動的型付けはプログラムの実行中に型検査を行うことができるので、柔軟なプログラミングが可能（プロトタイプ実装向け）であり、静的型付けはプログラム実行前に型検査を行うことで実行時にエラーが起こらないようにできるので、大規模なシステムの開発に向いています。これら二つの型付けを組み合わせることで両者の長所を持った検証システムの開発に取り組んでいます。

*1 プログラムの変数やサブルーチンの引数や返り値などの値の型を予め決めずに、プログラム実行時の実際の値によってプログラムが正しく動作しているかを検証する方法。

*2 プログラム実行前に、機能（関数）が形式に合った正しい型のデータのみを処理することを検証・保証する方法。

機械学習を活用したプログラミング言語理論研究

　今後チャレンジしたい研究は、「機械学習のためのプログラミング言語」として、機械学習を効率的に行えるよう確率や統計を取り入れたプログラミング言語の設計・開発です。もう一つはプログラムの安全性を保証するための「プログラミング言語のための機械学習」で、機械学習を活用してプログラムのバグ潰しを確実かつ効率的に行う研究をしたいと考えています。

　いずれも簡単ではありませんが、これから本格的に取り組み、最終的には機械学習を活用した自動的なバグ潰しと、プログラミングそのものの自動化に向けた研究を続けていきたいと思います。

大学3年生の頃、友人から紹介された型システム入門書の『Types and Programming Languages』を読んだことが、プログラミング言語理論の研究者になったきっかけだ。この本がプログラミング言語理論の面白さを教えてくれた。この本に出会わなかったら、今日の研究生活はなかったかもしれない。自分が面白いと思うことをこれからも追究していきたい。

リンク

• [NII Today] バグのないソフトウェアを目指して
• [NII SEEDS] 安全性と高生産性を両立したソフトウェア開発に向けて
• 「安心・安全なソフトウェアをめざして～プログラミング言語の科学」関山 太朗 NII研究100連発-2 オープンハウス2019