Verification mechanism in programming languages with dynamic modules

具有动态模块的编程语言中的验证机制

• 批准号: 23700029
• 负责人: KAMINA Tetsuo
• 金额: $ 2.08万
• 依托单位: The University of Tokyo
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Young Scientists (B)
• 财政年份: 2011
• 资助国家: 日本
• 起止时间: 2011 至 2012
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-23700029/
• 关键词: 文脈指向; 合成層; EventCJ; プログラム変換; 操作的意味論; 計算体系; イベント駆動; 暗黙的モジュール合成

Language mechanisms for dynamic module composition and their theories are studied through extending EventCJ, a context-oriented programming (COP) language with event-based per-instance layer transition. First, Featherweight EventCJ, a core calculus for EventCJ, is developed to formally define the operational semantics of EventCJ. Next, a new COP mechanism composite layers is developed to enhance the expressive power of representing relationship between contexts and layers (implementations of context-dependent behavior). Composite layers are implemented as a translation into EventCJ programs. By this translation, it is enabled to verify some properties about composite layers by applying the model-checking mechanism equipped with EventCJ. Finally, this translation is formally studied by extending Featherweight EventCJ with composite layers, and the theorem about the soundness of this translation is proven. Thus, it is ensured that the result of application of the model-checking mechanism in EventCJ is correct.

通过对EventCJ语言的扩展，研究了动态模块组合的语言机制及其理论。EventCJ是一种基于事件的逐实例层转换的面向上下文的程序设计语言。首先，Featherweight EventCJ，EventCJ的核心演算，被开发来形式化地定义EventCJ的操作语义。其次，提出了一种新的COP机制--复合层，以增强上下文和层之间关系的表达能力（上下文相关行为的实现）。复合层被实现为EventCJ程序的翻译。通过这种转换，它是能够验证复合层的一些属性，通过应用模型检查机制配备EventCJ。最后，通过对Featherweight EventCJ进行复合层扩展，形式化地研究了这种转换，并证明了这种转换的可靠性定理。从而保证了在EventCJ中应用模型检查机制的结果是正确的。

项目成果

Bridging Real-World Contexts and Units of Behavioral Variatios by Composite Layers.

通过复合层桥接现实世界环境和行为变化单元。

• 发表时间: 2012
• 期刊: In COP'12
• 作者: Tetsuo Kamina;Tomoyuki Aotani;and Hidehiko Masuhara.
• 通讯作者: and Hidehiko Masuhara.

JavaCat: Realizing Context as Fluent

JavaCat：实现上下文流畅

• 发表时间: 2013
• 作者: Keisuke Goto;Hideo Bannai;Shunsuke Inenaga;Masayuki Takeda;紙名哲生,青谷知幸,増原英彦.
• 通讯作者: 紙名哲生,青谷知幸,増原英彦.

文脈指向言語EventCJへの合成層の導入

向面向上下文的语言 EventCJ 引入组合层

• 发表时间: 2012
• 作者: Kouji Shimohira;Shunsuke Inenaga;Hideo Bannai;and Masayuki Takeda;黒野恵人，前田彩，河辺義信;紙名哲生,青谷知幸,増原英彦.
• 通讯作者: 紙名哲生,青谷知幸,増原英彦.

Featherweight EventCJ: a core calculus for a context-oriented language with event-based per-instance layer transition

Featherweight EventCJ：面向上下文的语言的核心演算，具有基于事件的每实例层转换

• DOI: 10.1145/2068736.2068737
• 发表时间: 2011
• 期刊: Proceedings of the Workshop onContext-Oriented Programming (COP'11)
• 作者: Tomoyuki Aotani;Tetsuo Kamina;Hidehiko Masuhara
• 通讯作者: Hidehiko Masuhara

Bridging real-world contexts and units of behavioral variations by composite layers

通过复合层桥接现实世界环境和行为变化单元

• DOI: 10.1145/2307436.2307440
• 发表时间: 2012
• 期刊: Proceedings of the Workshop on Context-Oriented Programming (COP'12)
• 作者: Tetsuo Kamina;Tomoyuki Aotani;Hidehiko Masuhara
• 通讯作者: Hidehiko Masuhara