|
文脈に依存したプログラムの振る舞いをモジュール化し、イベント駆動で動的にそれらを合成できる文脈指向プログラミング言語EventCJを対象に、動的モジュール合成のための言語機構および基礎理論に関する研究を行った。まず、EventCJの核言語Featherweight EventCJを構築し、その操作的意味論を形式的に定義した。それと同時に、事例研究により文脈とモジュールの対応関係を明らかにし、新たな一貫性保証のための言語機構として合成層を発明し、それをEventCJプログラムへの変換として実現した。これにより、EventCJに備わるモデル検査機構を用いることにより、モジュール合成に関する性質を検証することが可能になった。さらに、Featherweight EventCJを拡張して合成層の意味論及び元のFeatherweight EventCJへの変換を形式的に定義し、その変換が正しいという定理を証明した。これにより、合成層に関する性質をEventCJのモデル検査機構で検証した結果が、理論的に正しいということが保証された。
|
