| 研究課題/領域番号 |
16K16033
|
|---|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
青谷 知幸 東京工業大学, 情報理工学院, 助教 (20582919)
|
|---|
| 研究期間 (年度) |
2016-04-01 – 2019-03-31
|
| キーワード | 文脈指向プログラミング / mixin / 反応型プログラミング |
|---|
| 研究実績の概要 |
文脈に応じて振舞いを変えるプログラムのための基礎的な研究を行った．具体的には(1)センサからの情報に反応して計算を行う反応型プログラミング，(2)センサからの情報に反応して振舞いが切り替わる文脈指向プログラミングの検証技術，そして(3)ソースコードの文脈に依存してデータ構造を変える自動装飾を研究した．
反応型プログラミングは連続的に変化する実世界の情報を離散的な計算機で扱うためのプログラミング手法である．値の変化を取り扱うモデルとして，値を時間に対する関数として定義するもの(シグナルという)と，離散的なイベントで表現するものがあった．本研究ではこの両者を統合したモデルを提案し，代表的なオブジェクト指向言語であるJavaを拡張したSignalJを設計した．
文脈指向プログラミングは文脈に応じて振舞いを変えるプログラムの再利用性を高めるプログラミング手法である．基本的なアイデアは1つの関数に対して文脈ごとの定義を与えるものである．文脈指向ブログラミング言語の処理系は関数を実行する際，現在の文脈に照らし合わせて定義を選択する．このような関数の正しさには，文脈に依存しない正しさと，文脈ごとの正しさがある．本研究ではJavaプログラムの正しさを検証するJMLを拡張して，両方の正しさを定義・検証する手法を提案した．
装飾(mixin)は核となるデータ構造に機能を追加するものである．１つの装飾定義は複数の核データ構造に機能を追加することができ，プログラム開発が効率化できる．ネットワークストリームを表すデータ構造と，標準入出力を表すデータ構造に対する装飾の例として，バッファリングと暗号化が考えられる．装飾の考え方はプログラムの再利用性を向上させる一方，使いたいデータ構造を得るために多数の装飾を組合せなければならない問題があった．本研究では核データ構造の使われ方から装飾を推論する方法を提案した．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
共同研究を行う上で，研究計画の順序を変更した．プログラムの解析と検証技術の研究を3年目に行う予定であったが，JML研究の中心人物であるGary T. Leavens教授の協力が得られることになったため，前倒しをした．反応型プログラミングはセンサ情報に応じて挙動を変える文脈指向プログラミングの基礎となる．自動装飾はプログラム検証技術の一部である．センサ情報はプログラムの文脈を決定するが，プログラムがその文脈に対応できるとは限らない．自動装飾によってプログラムが対応できる文脈を推論することで，プログラムの文脈に対する網羅性や無矛盾性を検証することができる．
|
| 今後の研究の推進方策 |
反応型オブジェクト指向言語であるSignalJと，文脈指向プログラミングSerevalCJを融合させた言語SignalCJの研究を進める．またこれまでに提案したプログラム検証技術をSignalCJに応用して，SignalCJプログラムの検証技術を提案する．
|
| 次年度使用額が生じた理由 |
研究計画の順序を入れ替えたために，初年度に予定していた謝金と計算機の購入が先送りされた．
|
| 次年度使用額の使用計画 |
初年度の計画であった計算機の購入およびアプリケーション開発の謝金による使用を予定している．
|
