| 研究課題/領域番号 |
23700029
|
|---|
| 研究種目 |
若手研究(B)
|
| 配分区分 | 基金 |
|---|
| 研究分野 |
ソフトウエア
|
|---|
| 研究機関 | 東京大学 |
|---|
研究代表者 |
紙名 哲生 東京大学, 大学院・教育学研究科, 特任助教 (90431882)
|
|---|
| 研究期間 (年度) |
2011 – 2012
|
| 研究課題ステータス |
完了 (2012年度)
|
| 配分額 *注記 |
3,250千円 (直接経費: 2,500千円、間接経費: 750千円)
2012年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2011年度: 1,820千円 (直接経費: 1,400千円、間接経費: 420千円)
|
|---|
| キーワード | 文脈指向 / 合成層 / EventCJ / プログラム変換 / 操作的意味論 / 計算体系 / イベント駆動 / 暗黙的モジュール合成 |
|---|
| 研究概要 |
文脈に依存したプログラムの振る舞いをモジュール化し、イベント駆動で動的にそれらを合成できる文脈指向プログラミング言語EventCJを対象に、動的モジュール合成のための言語機構および基礎理論に関する研究を行った。まず、EventCJの核言語Featherweight EventCJを構築し、その操作的意味論を形式的に定義した。それと同時に、事例研究により文脈とモジュールの対応関係を明らかにし、新たな一貫性保証のための言語機構として合成層を発明し、それをEventCJプログラムへの変換として実現した。これにより、EventCJに備わるモデル検査機構を用いることにより、モジュール合成に関する性質を検証することが可能になった。さらに、Featherweight EventCJを拡張して合成層の意味論及び元のFeatherweight EventCJへの変換を形式的に定義し、その変換が正しいという定理を証明した。これにより、合成層に関する性質をEventCJのモデル検査機構で検証した結果が、理論的に正しいということが保証された。
|
