2012 Fiscal Year Annual Research Report
動的モジュールを持つプログラミング言語におけるソフトウェア検証機構
| Project/Area Number |
23700029
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
紙名 哲生 東京大学, 教育学研究科(研究院), 特任助教 (90431882)
|
|---|
| Keywords | 文脈指向 / 合成層 / EventCJ / プログラム変換 / 操作的意味論 |
|---|
| Research Abstract |
文脈に依存したプログラムの振る舞いをモジュール化し、イベント駆動で動的にそれらを合成できる文脈指向プログラミング言語EventCJを対象に、動的モジュール合成のための言語機構および基礎理論に関する研究を行った。最終年度においては、合成層と呼ばれる言語機構を発明し、それをEventCJ上で実現した。また、形式的な理論体系上においてその意味論を明らかにした。合成層はプログラム実行時の文脈とそれに対応するモジュールとの関係を記述するための機構であり、これにより文脈とモジュールとの関係が明らかになる。合成層の実現方法においては、既存のプログラミング言語EventCJのコードに変換するアルゴリズムを開発した。EventCJはモデル検査機構を提供しており、モジュール合成に関する性質を自動検証することが可能である。上述したアルゴリズムによって、合成層においても、変換後のEventCJのモデル検査機構を用いることにより、モジュール合成に関する性質を検証することが可能になった。さらに形式的な意味論上において、合成層からEventCJへの変換の正しさが証明された。これは、このアルゴリズムによって変換した後に行う検証結果が正しいことを保証するものである。
|
