• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Science of Computer Programming >Aspects preserving properties
【24h】

Aspects preserving properties

机译：保留属性的方面

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Aspect Oriented Programming can arbitrarily distort the semantics of programs. In particular, weaving can invalidate crucial safety and liveness properties of the base program. In this article, we identify categories of aspects that preserve some classes of properties. Specialized aspect languages are then designed to ensure that aspects belong to a specific category and, therefore, that woven programs will preserve the corresponding properties. Our categories of aspects, inspired by Katz's, comprise observers, aborters, confiners and weak intruders. Observers introduce new instructions and a new local state but they do not modify the base program's state and control-flow. Aborters are observers which may also abort executions. Confiners only ensure that executions remain in the reachable states of the base program. Weak intruders are confiners between two advice executions. These categories (along with two others) are defined formally based on a language independent abstract semantics framework. The classes of preserved properties are defined as subsets of LTL for deterministic programs and CTL' for non-deterministic ones. We can formally prove that, for any program, the weaving of any aspect in a category preserves any property in the related class. We present, for most aspect categories, a specialized aspect language which ensures that any aspect written in that language belongs to the corresponding category. It can be proved that these languages preserve the corresponding classes of properties by construction. The aspect languages share the same expressive pointcut language and are designed w.r.t. a common imperative base language. Each category and language is illustrated by simple examples. The appendix provides semantics and two instances of proofs: the proof of preservation of properties by a category and the proof that all aspects written in a language belong to the corresponding category.
机译：面向方面的编程可以任意扭曲程序的语义。特别是，编织可能会使基本程序的关键安全性和活动性无效。在本文中，我们确定保留某些属性类别的方面的类别。然后设计专门的方面语言，以确保方面属于特定类别，因此，编织程序将保留相应的属性。受卡兹（Katz）启发，我们的方面类别包括观察员，堕胎者，限制者和弱势入侵者。观察者会引入新的指令和新的本地状态，但不会修改基本程序的状态和控制流。中止者是观察者，也可能中止执行。限制器仅确保执行保持在基本程序的可到达状态。弱入侵者是两个建议执行之间的限制者。这些类别（以及其他两个类别）是基于独立于语言的抽象语义框架正式定义的。保留属性的类别被定义为确定性程序的LTL子集和非确定性程序的CTL'。我们可以正式证明，对于任何程序，类别中任何方面的编织都可以保留相关类中的任何属性。对于大多数方面类别，我们提供一种专门的方面语言，以确保用该语言编写的任何方面都属于相应的类别。可以证明，这些语言通过构造保留了相应的属性类。方面语言共享相同的表达切入点语言，并且经过精心设计。常见的命令式基本语言。每个类别和语言都通过简单的示例进行说明。附录提供了语义和证明的两个实例：按类别保存属性的证明和用语言编写的所有方面都属于相应类别的证明。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号