2011 Fiscal Year Research-status Report
動的モジュールを持つプログラミング言語におけるソフトウェア検証機構
| Project/Area Number |
23700029
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
紙名 哲生 東京大学, 教育学研究科(研究院), 特任助教 (90431882)
|
|---|
| Project Period (FY) |
2011-04-28 – 2013-03-31
|
| Keywords | 文脈指向 / 計算体系 / イベント駆動 / EventCJ / 暗黙的モジュール合成 |
|---|
| Research Abstract |
文脈に依存したプログラムの振る舞いをモジュール化し、イベント駆動で動的にそれらを合成できる文脈指向プログラミング言語EventCJを対象に、動的モジュール合成のための基礎理論に関する研究を行った。具体的には、EventCJの核言語Featherweight EventCJを提案し、その操作的意味論を形式的に定義した。文脈指向言語の理論的な計算体系としては先にContextFJが提案されていたが、Featherweight EventCJは、イベント駆動に個々のインスタンスの振る舞いを宣言的に記述された規則に基づいて動的に変更させるという、より先進的な動的モジュール合成のメカニズムの意味論を形式化した点において独自性がある。これにより、複数のイベントが同時に生成された場合や、適用可能なモジュール合成の規則が複数存在した場合などにおいて、EventCJがどのように振る舞うかが明らかにされた。このことにより、次年度に計画されているプログラム検証に関する研究のための堅牢な理論的基礎が与えられた。また、事例研究により文脈とモジュールの対応関係が明らかになり、新たな一貫性保証のための言語機構を実現できる可能性が出てきた。モジュールは文脈と一対一対応するアトミックなモジュールを基に、それらの組み合わせ（論理和・論理積・論理差）によってさらに高次なモジュールが合成される複雑な関係を持っている。合成モジュールが、それの依存する他のモジュールの活性状態によって暗黙的に合成される言語機構を実現することにより、動的モジュール合成に関するある種の一貫性を保証できる。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初の計画どおり、EventCJの形式的意味論を明らかにすることができた。また、事例研究により、当初の計画には含まれていない新たな暗黙的モジュール合成の機構とそれによる一貫性保証についての構想を得ることができた。
|
| Strategy for Future Research Activity |
当初の計画通り、EventCJのためのプログラム検証に関する研究を進める。また、新たに得られた暗黙的モジュール合成のための言語機構に関する構想について、それを具現化するための研究を行う。
|
| Expenditure Plans for the Next FY Research Funding |
物品費、旅費ともに多少の残額が発生した。次年度の研究費と合わせて、今後の研究の推進のために使用する計画である。
|
