| 研究課題/領域番号 |
19K20245
|
|---|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
森口 草介 東京工業大学, 情報理工学院, 助教 (60733409)
|
|---|
| 研究期間 (年度) |
2019-04-01 – 2022-03-31
|
| キーワード | 型システム / プログラム意味論 |
|---|
| 研究実績の概要 |
ソースコードを直接扱う言語には、数の表現以外に構造を持ったデータ表現が必須と言える。ほとんどの汎用言語では配列やデータ構造を定義できるため問題とはならないが、領域特化言語のうち、特に計算能力を制限することで計算資源に関する特性を得ている場合、データ表現またはそれに付随する操作の実現可能範囲が狭く、ソースコードをプログラム上に表現することは難しい。
本研究課題の目的はソースコードを操作するプログラムを検証することであるが、その条件はソースコードをプログラム上に表現できることである。そのため、プログラミング言語の拡張により本課題の適用可能範囲が拡大する。
2020年度はこの問題に対する二つの研究成果を報告した。これらは関数リアクティブプログラミング言語を対象に、一つは配列を導入、もう一つは再帰的データ構造を導入したものである。これらにより、領域特化言語を含むより広い範囲の言語にソースコード相当の表現が可能になった。以下にそれぞれの詳細を説明する。
配列については、範囲外アクセスに対して多くの言語がエラーや例外を発生させるが、提案手法ではアクセスの結果を代替値を提示することでエラーや例外なしに処理を続行できる仕組みを構築した。
再帰的データ構造については、型システムに各データ構造の取り得る最大サイズを持たせたBounded Construction Type（以下BCT）を導入した。データを操作する再帰関数の停止性を保証できる他、実行時に実際の大きさが既定の大きさと異なるかを比較できる仕組みが備わっており、より処理時間やデータ構造が用いるメモリサイズを意識したプログラミングが可能となっている。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
本来の研究計画にて述べていた手法について、構築そのものは出来ているものの、成果として検証するソフトウェアの性質を表現できる意味論を構築していなかったため、全体を再構築中である。そのため論文やライブラリの公開に遅れが発生している。
|
| 今後の研究の推進方策 |
元々の手法に加えて、関数リアクティブプログラミング言語を題材としたメタプログラミングの形式化を行う。この追加課題については、既に関数リアクティブプログラミング言語の形式化を行っているRAとともに進める。
|
| 次年度使用額が生じた理由 |
昨年度のRA雇用を取りやめたが、本年度は新たに設定したリアクティブプログラミングに対するメタプログラミングの形式化と検証を進めるためにRAを雇用する予定である。
|
