研究シーズ2016ソフトウェア科学

信頼性の高いプログラムを容易に記述するための型エラーデバッグ手法

対馬 かなえアーキテクチャ科学研究系 助教

研究分野関数プログラミング/プログラミング言語/デバッグ手法

研究背景・目的

小学校でプログラミングの授業が導入されたことが話題になるなど、プログラミングは特殊な技能ではなく、一般に広く使用される技術へと変わりつつあります。同時に、プログラムは我々の生活のあちこちに深く溶け込んでおり、安全に動作する事を保証することは重要です。よって、これからは安全なプログラムを初心者のプログラマでも書けるようにすることは必要不可欠といえます。

このような背景のもと、我々はプログラムの安全性を保証する一つの手法である「型」に着目しました。型によって、安全でないプログラムは「型エラー」として排除されるためプログラムの安全性は保証される一方で、正しいプログラムを書く事は難しくなります。そのような場合にも、型エラーを容易に修正できる方法が提供されていれば、初心者でも簡単に安全なプログラムを書く事ができるようになります。

研究内容

これまでの型エラーデバッグ手法が、小さな言語での実験的なものにとどまっていることを問題として捉え、実用的な言語で実装するための手法を研究しています。

既存のコンパイラの機能をうまく再利用するというアイデア(下の図)を使うことで、デバッグ手法自体の実装量を削減し、コンパイラの仕様変更への対応を容易にすることができました。

4-1_tsushima_1.jpg

本研究のアイデア

具体的には以下の三手法を提案・実装しました。

  1. 対話的に型エラーの原因を探す型エラーデバッガ:デバッガの質問に繰り返し答えていくと、デバッガが自動的にエラーの原因を特定します。
  2. 型エラーになる最小の範囲を求める型エラースライサ:型エラーの原因が含まれる可能性がある箇所を絞り込むことができます。
  3. 複数のエラーメッセージの作成:通常のコンパイラより多くのエラーメッセージを返すことで、プログラマが自分で役に立つものを選ぶことができます。

4-1_tsushima_2.jpg

(1)型エラーデバッガ

4-1_tsushima_3.jpg

(2)型エラースライス

4-1_tsushima_4.jpg

(3)複数の型エラーメッセージの作成

産業応用の可能性

連絡先

対馬 かなえ[アーキテクチャ科学研究系 助教]
k_tsushima[at]nii.ac.jp ※[at]を@に変換してください

Recommend

さらにみる